chore(LinearAlgebra): split Quotient.lean into Defs and Basic (#…

…18384)

This PR rearranges the definitions of quotient modules as follows:
 * `LinearAlgebra/QuotientPi.lean` is renamed `LinearAlgebra/Quotient/Pi.lean`
 * `LinearAlgebra/Quotient.lean` is split into
   - `LinearAlgebra/Quotient/Defs.lean` (with the definition and module structure of the quotient module)
   - `LinearAlgebra/Quotient/Basic.lean` (with some basic maps for the quotient)

Mathlib.lean

@@ -3233,8 +3233,9 @@ import Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric
 import Mathlib.LinearAlgebra.QuadraticForm.Real
 import Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
 import Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
-import Mathlib.LinearAlgebra.Quotient
-import Mathlib.LinearAlgebra.QuotientPi
+import Mathlib.LinearAlgebra.Quotient.Basic
+import Mathlib.LinearAlgebra.Quotient.Defs
+import Mathlib.LinearAlgebra.Quotient.Pi
 import Mathlib.LinearAlgebra.Ray
 import Mathlib.LinearAlgebra.Reflection
 import Mathlib.LinearAlgebra.RootSystem.Basic

Mathlib/Algebra/Category/ModuleCat/EpiMono.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
-import Mathlib.LinearAlgebra.Quotient
+import Mathlib.LinearAlgebra.Quotient.Basic
 import Mathlib.Algebra.Category.ModuleCat.Basic
 import Mathlib.CategoryTheory.ConcreteCategory.EpiMono
 

Mathlib/Algebra/DirectLimit.lean

@@ -3,8 +3,9 @@ Copyright (c) 2019 Kenny Lau, Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Chris Hughes, Jujian Zhang
 -/
-import Mathlib.Data.Finset.Order
 import Mathlib.Algebra.DirectSum.Module
+import Mathlib.Data.Finset.Order
+import Mathlib.LinearAlgebra.Quotient.Basic
 import Mathlib.RingTheory.FreeCommRing
 import Mathlib.RingTheory.Ideal.Maps
 import Mathlib.RingTheory.Ideal.Quotient

Mathlib/Algebra/Exact.lean

@@ -6,7 +6,7 @@ Authors: Antoine Chambert-Loir
 
 import Mathlib.Algebra.Module.Submodule.Range
 import Mathlib.LinearAlgebra.Prod
-import Mathlib.LinearAlgebra.Quotient
+import Mathlib.LinearAlgebra.Quotient.Basic
 
 /-! # Exactness of a pair
 

Mathlib/Algebra/Module/Presentation/Basic.lean

@@ -6,7 +6,7 @@ Authors: Joël Riou
 import Mathlib.Algebra.Exact
 import Mathlib.Algebra.Module.Basic
 import Mathlib.LinearAlgebra.Finsupp
-import Mathlib.LinearAlgebra.Quotient
+import Mathlib.LinearAlgebra.Quotient.Basic
 
 /-!
 # Presentations of modules

Mathlib/Algebra/Module/Submodule/Localization.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import Mathlib.Algebra.Module.LocalizedModule
-import Mathlib.LinearAlgebra.Quotient
+import Mathlib.LinearAlgebra.Quotient.Basic
 import Mathlib.RingTheory.Localization.Module
 
 /-!

Mathlib/LinearAlgebra/FreeModule/IdealQuotient.lean

@@ -6,7 +6,7 @@ Authors: Anne Baanen
 import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
 import Mathlib.LinearAlgebra.FreeModule.PID
 import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
-import Mathlib.LinearAlgebra.QuotientPi
+import Mathlib.LinearAlgebra.Quotient.Pi
 import Mathlib.RingTheory.Ideal.Basis
 import Mathlib.LinearAlgebra.Dimension.Constructions
 

Mathlib/LinearAlgebra/Isomorphisms.lean

@@ -3,7 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov
 -/
-import Mathlib.LinearAlgebra.Quotient
+import Mathlib.LinearAlgebra.Quotient.Basic
 
 /-!
 # Isomorphism theorems for modules.

Mathlib/LinearAlgebra/Projection.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.LinearAlgebra.Quotient
+import Mathlib.LinearAlgebra.Quotient.Basic
 import Mathlib.LinearAlgebra.Prod
 
 /-!

Mathlib/LinearAlgebra/Quotient.lean → Mathlib/LinearAlgebra/Quotient/Basic.lean

@@ -3,10 +3,11 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov
 -/
-import Mathlib.LinearAlgebra.Span
-import Mathlib.LinearAlgebra.Pi
 import Mathlib.Algebra.Module.Equiv.Basic
 import Mathlib.GroupTheory.QuotientGroup.Basic
+import Mathlib.LinearAlgebra.Pi
+import Mathlib.LinearAlgebra.Quotient.Defs
+import Mathlib.LinearAlgebra.Span
 import Mathlib.SetTheory.Cardinal.Finite
 
 /-!
@@ -15,6 +16,14 @@ import Mathlib.SetTheory.Cardinal.Finite
 * If `p` is a submodule of `M`, `M ⧸ p` is the quotient of `M` with respect to `p`:
   that is, elements of `M` are identified if their difference is in `p`. This is itself a module.
 
+## Main definitions
+
+* `Submodule.Quotient.restrictScalarsEquiv`: The quotient of `P` as an `S`-submodule is the same
+  as the quotient of `P` as an `R`-submodule,
+* `Submodule.liftQ`: lift a map `M → M₂` to a map `M ⧸ p → M₂` if the kernel is contained in `p`
+* `Submodule.mapQ`: lift a map `M → M₂` to a map `M ⧸ p → M₂ ⧸ q` if the image of `p` is contained
+  in `q`
+
 -/
 
 -- For most of this file we work over a noncommutative ring
@@ -27,174 +36,11 @@ variable (p p' : Submodule R M)
 
 open LinearMap QuotientAddGroup
 
-/-- The equivalence relation associated to a submodule `p`, defined by `x ≈ y` iff `-x + y ∈ p`.
-
-Note this is equivalent to `y - x ∈ p`, but defined this way to be defeq to the `AddSubgroup`
-version, where commutativity can't be assumed. -/
-def quotientRel : Setoid M :=
-  QuotientAddGroup.leftRel p.toAddSubgroup
-
-theorem quotientRel_def {x y : M} : p.quotientRel x y ↔ x - y ∈ p :=
-  Iff.trans
-    (by
-      rw [leftRel_apply, sub_eq_add_neg, neg_add, neg_neg]
-      rfl)
-    neg_mem_iff
-
-@[deprecated (since := "2024-08-29")] alias quotientRel_r_def := quotientRel_def
-
-/-- The quotient of a module `M` by a submodule `p ⊆ M`. -/
-instance hasQuotient : HasQuotient M (Submodule R M) :=
-  ⟨fun p => Quotient (quotientRel p)⟩
-
 namespace Quotient
 
-/-- Map associating to an element of `M` the corresponding element of `M/p`,
-when `p` is a submodule of `M`. -/
-def mk {p : Submodule R M} : M → M ⧸ p :=
-  Quotient.mk''
-
-theorem mk'_eq_mk' {p : Submodule R M} (x : M) :
-    @Quotient.mk' _ (quotientRel p) x = mk x :=
-  rfl
-
-theorem mk''_eq_mk {p : Submodule R M} (x : M) : (Quotient.mk'' x : M ⧸ p) = mk x :=
-  rfl
-
-theorem quot_mk_eq_mk {p : Submodule R M} (x : M) : (Quot.mk _ x : M ⧸ p) = mk x :=
-  rfl
-
-protected theorem eq' {x y : M} : (mk x : M ⧸ p) = mk y ↔ -x + y ∈ p :=
-  QuotientAddGroup.eq
-
-protected theorem eq {x y : M} : (mk x : M ⧸ p) = mk y ↔ x - y ∈ p :=
-  (Submodule.Quotient.eq' p).trans (leftRel_apply.symm.trans p.quotientRel_def)
-
-instance : Zero (M ⧸ p) where
-  -- Use Quotient.mk'' instead of mk here because mk is not reducible.
-  -- This would lead to non-defeq diamonds.
-  -- See also the same comment at the One instance for Con.
-  zero := Quotient.mk'' 0
-
-instance : Inhabited (M ⧸ p) :=
-  ⟨0⟩
-
-@[simp]
-theorem mk_zero : mk 0 = (0 : M ⧸ p) :=
-  rfl
-
-@[simp]
-theorem mk_eq_zero : (mk x : M ⧸ p) = 0 ↔ x ∈ p := by simpa using (Quotient.eq' p : mk x = 0 ↔ _)
-
-instance addCommGroup : AddCommGroup (M ⧸ p) :=
-  QuotientAddGroup.Quotient.addCommGroup p.toAddSubgroup
-
-@[simp]
-theorem mk_add : (mk (x + y) : M ⧸ p) = mk x + mk y :=
-  rfl
-
-@[simp]
-theorem mk_neg : (mk (-x) : M ⧸ p) = -(mk x) :=
-  rfl
-
-@[simp]
-theorem mk_sub : (mk (x - y) : M ⧸ p) = mk x - mk y :=
-  rfl
-
-protected nonrec lemma «forall» {P : M ⧸ p → Prop} : (∀ a, P a) ↔ ∀ a, P (mk a) := Quotient.forall
-
-section SMul
-
-variable {S : Type*} [SMul S R] [SMul S M] [IsScalarTower S R M] (P : Submodule R M)
-
-instance instSMul' : SMul S (M ⧸ P) :=
-  ⟨fun a =>
-    Quotient.map' (a • ·) fun x y h =>
-      leftRel_apply.mpr <| by simpa using Submodule.smul_mem P (a • (1 : R)) (leftRel_apply.mp h)⟩
-
--- Porting note: should this be marked as a `@[default_instance]`?
-/-- Shortcut to help the elaborator in the common case. -/
-instance instSMul : SMul R (M ⧸ P) :=
-  Quotient.instSMul' P
-
-@[simp]
-theorem mk_smul (r : S) (x : M) : (mk (r • x) : M ⧸ p) = r • mk x :=
-  rfl
-
-instance smulCommClass (T : Type*) [SMul T R] [SMul T M] [IsScalarTower T R M]
-    [SMulCommClass S T M] : SMulCommClass S T (M ⧸ P) where
-  smul_comm _x _y := Quotient.ind' fun _z => congr_arg mk (smul_comm _ _ _)
-
-instance isScalarTower (T : Type*) [SMul T R] [SMul T M] [IsScalarTower T R M] [SMul S T]
-    [IsScalarTower S T M] : IsScalarTower S T (M ⧸ P) where
-  smul_assoc _x _y := Quotient.ind' fun _z => congr_arg mk (smul_assoc _ _ _)
-
-instance isCentralScalar [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [IsScalarTower Sᵐᵒᵖ R M]
-    [IsCentralScalar S M] : IsCentralScalar S (M ⧸ P) where
-  op_smul_eq_smul _x := Quotient.ind' fun _z => congr_arg mk <| op_smul_eq_smul _ _
-
-end SMul
-
 section Module
 
-variable {S : Type*}
-
--- Performance of `Function.Surjective.mulAction` is worse since it has to unify data to apply
--- TODO: leanprover-community/mathlib4#7432
-instance mulAction' [Monoid S] [SMul S R] [MulAction S M] [IsScalarTower S R M]
-    (P : Submodule R M) : MulAction S (M ⧸ P) :=
-  { Function.Surjective.mulAction mk (surjective_quot_mk _) <| Submodule.Quotient.mk_smul P with
-    toSMul := instSMul' _ }
-
--- Porting note: should this be marked as a `@[default_instance]`?
-instance mulAction (P : Submodule R M) : MulAction R (M ⧸ P) :=
-  Quotient.mulAction' P
-
-instance smulZeroClass' [SMul S R] [SMulZeroClass S M] [IsScalarTower S R M] (P : Submodule R M) :
-    SMulZeroClass S (M ⧸ P) :=
-  ZeroHom.smulZeroClass ⟨mk, mk_zero _⟩ <| Submodule.Quotient.mk_smul P
-
--- Porting note: should this be marked as a `@[default_instance]`?
-instance smulZeroClass (P : Submodule R M) : SMulZeroClass R (M ⧸ P) :=
-  Quotient.smulZeroClass' P
-
--- Performance of `Function.Surjective.distribSMul` is worse since it has to unify data to apply
--- TODO: leanprover-community/mathlib4#7432
-instance distribSMul' [SMul S R] [DistribSMul S M] [IsScalarTower S R M] (P : Submodule R M) :
-    DistribSMul S (M ⧸ P) :=
-  { Function.Surjective.distribSMul {toFun := mk, map_zero' := rfl, map_add' := fun _ _ => rfl}
-    (surjective_quot_mk _) (Submodule.Quotient.mk_smul P) with
-    toSMulZeroClass := smulZeroClass' _ }
-
--- Porting note: should this be marked as a `@[default_instance]`?
-instance distribSMul (P : Submodule R M) : DistribSMul R (M ⧸ P) :=
-  Quotient.distribSMul' P
-
--- Performance of `Function.Surjective.distribMulAction` is worse since it has to unify data
--- TODO: leanprover-community/mathlib4#7432
-instance distribMulAction' [Monoid S] [SMul S R] [DistribMulAction S M] [IsScalarTower S R M]
-    (P : Submodule R M) : DistribMulAction S (M ⧸ P) :=
-  { Function.Surjective.distribMulAction {toFun := mk, map_zero' := rfl, map_add' := fun _ _ => rfl}
-    (surjective_quot_mk _) (Submodule.Quotient.mk_smul P) with
-    toMulAction := mulAction' _ }
-
--- Porting note: should this be marked as a `@[default_instance]`?
-instance distribMulAction (P : Submodule R M) : DistribMulAction R (M ⧸ P) :=
-  Quotient.distribMulAction' P
-
--- Performance of `Function.Surjective.module` is worse since it has to unify data to apply
--- TODO: leanprover-community/mathlib4#7432
-instance module' [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] (P : Submodule R M) :
-    Module S (M ⧸ P) :=
-  { Function.Surjective.module _ {toFun := mk, map_zero' := by rfl, map_add' := fun _ _ => by rfl}
-    (surjective_quot_mk _) (Submodule.Quotient.mk_smul P) with
-    toDistribMulAction := distribMulAction' _ }
-
--- Porting note: should this be marked as a `@[default_instance]`?
-instance module (P : Submodule R M) : Module R (M ⧸ P) :=
-  Quotient.module' P
-
-variable (S)
+variable (S : Type*)
 
 /-- The quotient of `P` as an `S`-submodule is the same as the quotient of `P` as an `R`-submodule,
 where `P : Submodule R M`.
@@ -219,10 +65,6 @@ theorem restrictScalarsEquiv_symm_mk [Ring S] [SMul S R] [Module S M] [IsScalarT
 
 end Module
 
-theorem mk_surjective : Function.Surjective (@mk _ _ _ _ _ p) := by
-  rintro ⟨x⟩
-  exact ⟨x, rfl⟩
-
 theorem nontrivial_of_lt_top (h : p < ⊤) : Nontrivial (M ⧸ p) := by
   obtain ⟨x, _, not_mem_s⟩ := SetLike.exists_of_lt h
   refine ⟨⟨mk x, 0, ?_⟩⟩
@@ -270,23 +112,6 @@ section
 
 variable {M₂ : Type*} [AddCommGroup M₂] [Module R M₂]
 
-theorem quot_hom_ext (f g : (M ⧸ p) →ₗ[R] M₂) (h : ∀ x : M, f (Quotient.mk x) = g (Quotient.mk x)) :
-    f = g :=
-  LinearMap.ext fun x => Quotient.inductionOn' x h
-
-/-- The map from a module `M` to the quotient of `M` by a submodule `p` as a linear map. -/
-def mkQ : M →ₗ[R] M ⧸ p where
-  toFun := Quotient.mk
-  map_add' := by simp
-  map_smul' := by simp
-
-@[simp]
-theorem mkQ_apply (x : M) : p.mkQ x = Quotient.mk x :=
-  rfl
-
-theorem mkQ_surjective : Function.Surjective p.mkQ := by
-  rintro ⟨x⟩; exact ⟨x, rfl⟩
-
 theorem strictMono_comap_prod_map :
     StrictMono fun m : Submodule R M ↦ (m.comap p.subtype, m.map p.mkQ) :=
   fun m₁ m₂ ↦ QuotientAddGroup.strictMono_comap_prod_map
@@ -296,14 +121,6 @@ end
 
 variable {R₂ M₂ : Type*} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂}
 
-/-- Two `LinearMap`s from a quotient module are equal if their compositions with
-`submodule.mkQ` are equal.
-
-See note [partially-applied ext lemmas]. -/
-@[ext 1100] -- Porting note: increase priority so this applies before `LinearMap.ext`
-theorem linearMap_qext ⦃f g : M ⧸ p →ₛₗ[τ₁₂] M₂⦄ (h : f.comp p.mkQ = g.comp p.mkQ) : f = g :=
-  LinearMap.ext fun x => Quotient.inductionOn' x <| (LinearMap.congr_fun h : _)
-
 /-- The map from the quotient of `M` by a submodule `p` to `M₂` induced by a linear map `f : M → M₂`
 vanishing on `p`, as a linear map. -/
 def liftQ (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ ker f) : M ⧸ p →ₛₗ[τ₁₂] M₂ :=
@@ -559,24 +376,6 @@ theorem coe_quotEquivOfEqBot_symm (hp : p = ⊥) :
     ((p.quotEquivOfEqBot hp).symm : M →ₗ[R] M ⧸ p) = p.mkQ :=
   rfl
 
-/-- Quotienting by equal submodules gives linearly equivalent quotients. -/
-def quotEquivOfEq (h : p = p') : (M ⧸ p) ≃ₗ[R] M ⧸ p' :=
-  { @Quotient.congr _ _ (quotientRel p) (quotientRel p') (Equiv.refl _) fun a b => by
-      subst h
-      rfl with
-    map_add' := by
-      rintro ⟨x⟩ ⟨y⟩
-      rfl
-    map_smul' := by
-      rintro x ⟨y⟩
-      rfl }
-
-@[simp]
-theorem quotEquivOfEq_mk (h : p = p') (x : M) :
-    Submodule.quotEquivOfEq p p' h (Submodule.Quotient.mk x) =
-      (Submodule.Quotient.mk x) :=
-  rfl
-
 @[simp]
 theorem Quotient.equiv_refl (P : Submodule R M) (Q : Submodule R M)
     (hf : P.map (LinearEquiv.refl R M : M →ₗ[R] M) = Q) :