Mathlib.LinearAlgebra.Quotient.Defs

Submodule.quotientRel definition

: Setoid M

Full source

/-- 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

Equivalence relation induced by a submodule

Informal description

The equivalence relation on a module $M$ induced by a submodule $p$, where two elements $x, y \in M$ are equivalent if and only if their difference $x - y$ belongs to $p$. This relation is defined as $x \approx y \iff x - y \in p$.

Submodule.quotientRel_def theorem

{x y : M} : p.quotientRel x y ↔ x - y ∈ p

Full source

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

Characterization of Quotient Relation by Submodule Membership

Informal description

For any elements $x, y$ in a module $M$ and a submodule $p$ of $M$, the equivalence relation $x \approx y$ holds if and only if their difference $x - y$ belongs to $p$.

Submodule.hasQuotient instance

: HasQuotient M (Submodule R M)

Full source

/-- The quotient of a module `M` by a submodule `p ⊆ M`. -/
instance hasQuotient : HasQuotient M (Submodule R M) :=
  ⟨fun p => Quotient (quotientRel p)⟩

Quotient Module by a Submodule

Informal description

For any module $M$ over a ring $R$ and any submodule $p$ of $M$, the quotient $M ⧸ p$ is defined as the set of equivalence classes of elements of $M$ under the relation $x \sim y$ if and only if $x - y \in p$.

Submodule.Quotient.mk definition

{p : Submodule R M} : M → M ⧸ p

Full source

/-- 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''

Quotient map from module to quotient module

Informal description

The function maps an element $x$ of a module $M$ to its equivalence class $[x]$ in the quotient module $M ⧸ p$, where $p$ is a submodule of $M$ and two elements are equivalent if their difference belongs to $p$.

Submodule.Quotient.mk'_eq_mk' theorem

{p : Submodule R M} (x : M) : @Quotient.mk' _ (quotientRel p) x = mk x

Full source

theorem mk'_eq_mk' {p : Submodule R M} (x : M) :
    @Quotient.mk' _ (quotientRel p) x = mk x :=
  rfl

Equality of Quotient Constructions for Submodules

Informal description

For any submodule $p$ of a module $M$ over a ring $R$, and for any element $x \in M$, the equivalence class of $x$ under the quotient relation induced by $p$ (denoted by $\text{Quotient.mk'}$) is equal to the image of $x$ under the quotient map $\text{mk}$ from $M$ to $M ⧸ p$.

Submodule.Quotient.mk''_eq_mk theorem

{p : Submodule R M} (x : M) : (Quotient.mk'' x : M ⧸ p) = mk x

Full source

theorem mk''_eq_mk {p : Submodule R M} (x : M) : (Quotient.mk'' x : M ⧸ p) = mk x :=
  rfl

Equivalence of Quotient Constructions in Module Quotient

Informal description

For any element $x$ of a module $M$ and any submodule $p$ of $M$, the equivalence class of $x$ in the quotient module $M ⧸ p$ constructed via `Quotient.mk''` is equal to the equivalence class constructed via `mk`.

Submodule.Quotient.quot_mk_eq_mk theorem

{p : Submodule R M} (x : M) : (Quot.mk _ x : M ⧸ p) = mk x

Full source

theorem quot_mk_eq_mk {p : Submodule R M} (x : M) : (Quot.mk _ x : M ⧸ p) = mk x :=
  rfl

Equivalence of Quotient Constructions in Module Quotient

Informal description

For any element $x$ in a module $M$ and any submodule $p$ of $M$, the equivalence class of $x$ in the quotient module $M ⧸ p$ constructed via `Quot.mk` is equal to the equivalence class constructed via the quotient map `mk`.

Submodule.Quotient.eq' theorem

{x y : M} : (mk x : M ⧸ p) = mk y ↔ -x + y ∈ p

Full source

protected theorem eq' {x y : M} : (mk x : M ⧸ p) = mk y ↔ -x + y ∈ p :=
  QuotientAddGroup.eq

Equivalence in Quotient Module via Submodule Condition

Informal description

For any elements $x, y$ in a module $M$ over a ring $R$ and a submodule $p$ of $M$, the equivalence classes $[x]$ and $[y]$ in the quotient module $M ⧸ p$ are equal if and only if $-x + y \in p$.

Submodule.Quotient.eq theorem

{x y : M} : (mk x : M ⧸ p) = mk y ↔ x - y ∈ p

Full source

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)

Equivalence in Quotient Module via Difference in Submodule

Informal description

For any elements $x, y$ in a module $M$ over a ring $R$ and a submodule $p$ of $M$, the equivalence classes $[x]$ and $[y]$ in the quotient module $M ⧸ p$ are equal if and only if their difference $x - y$ belongs to $p$.

Submodule.Quotient.instZeroQuotient instance

: Zero (M ⧸ p)

Full source

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

Zero Element in Quotient Module

Informal description

The quotient module $M ⧸ p$ has a zero element, which is the equivalence class of the zero element of $M$.

Submodule.Quotient.instInhabitedQuotient instance

: Inhabited (M ⧸ p)

Full source

instance : Inhabited (M ⧸ p) :=
  ⟨0⟩

Quotient Module is Inhabited

Informal description

For any module $M$ over a ring $R$ and any submodule $p$ of $M$, the quotient module $M ⧸ p$ is inhabited (i.e., it contains at least one element).

Submodule.Quotient.mk_zero theorem

: mk 0 = (0 : M ⧸ p)

Full source

@[simp]
theorem mk_zero : mk 0 = (0 : M ⧸ p) :=
  rfl

Quotient Map Preserves Zero: $\operatorname{mk}(0) = 0$

Informal description

The equivalence class of the zero element in $M$ under the quotient map $\operatorname{mk} : M \to M ⧸ p$ is equal to the zero element in the quotient module $M ⧸ p$, i.e., $\operatorname{mk}(0) = 0$.

Submodule.Quotient.mk_eq_zero theorem

: (mk x : M ⧸ p) = 0 ↔ x ∈ p

Full source

@[simp]
theorem mk_eq_zero : (mk x : M ⧸ p) = 0 ↔ x ∈ p := by simpa using (Quotient.eq' p : mkmk x = 0 ↔ _)

Characterization of Zero in Quotient Module: $[x] = 0 \leftrightarrow x \in p$

Informal description

For any element $x$ of a module $M$ over a ring $R$ and a submodule $p$ of $M$, the equivalence class of $x$ in the quotient module $M ⧸ p$ is equal to zero if and only if $x$ belongs to $p$.

Submodule.Quotient.addCommGroup instance

: AddCommGroup (M ⧸ p)

Full source

instance addCommGroup : AddCommGroup (M ⧸ p) :=
  QuotientAddGroup.Quotient.addCommGroup p.toAddSubgroup

Additive Commutative Group Structure on Quotient Module $M ⧸ p$

Informal description

For any module $M$ over a ring $R$ and any submodule $p$ of $M$, the quotient module $M ⧸ p$ forms an additive commutative group.

Submodule.Quotient.mk_add theorem

: (mk (x + y) : M ⧸ p) = mk x + mk y

Full source

@[simp]
theorem mk_add : (mk (x + y) : M ⧸ p) = mk x + mk y :=
  rfl

Additivity of Quotient Module Map: $[x + y] = [x] + [y]$

Informal description

For any elements $x$ and $y$ of a module $M$ over a ring $R$ and a submodule $p$ of $M$, the equivalence class of the sum $x + y$ in the quotient module $M ⧸ p$ is equal to the sum of the equivalence classes of $x$ and $y$, i.e., $[x + y] = [x] + [y]$.

Submodule.Quotient.mk_neg theorem

: (mk (-x) : M ⧸ p) = -(mk x)

Full source

@[simp]
theorem mk_neg : (mk (-x) : M ⧸ p) = -(mk x) :=
  rfl

Negation Commutes with Quotient Map: $[-x] = -[x]$

Informal description

For any element $x$ of a module $M$ over a ring $R$ and any submodule $p$ of $M$, the equivalence class of $-x$ in the quotient module $M ⧸ p$ is equal to the negation of the equivalence class of $x$, i.e., $[-x] = -[x]$.

Submodule.Quotient.mk_sub theorem

: (mk (x - y) : M ⧸ p) = mk x - mk y

Full source

@[simp]
theorem mk_sub : (mk (x - y) : M ⧸ p) = mk x - mk y :=
  rfl

Quotient Module Preserves Subtraction: $[x - y] = [x] - [y]$

Informal description

For any elements $x$ and $y$ of a module $M$ over a ring $R$, and any submodule $p$ of $M$, the equivalence class of $x - y$ in the quotient module $M ⧸ p$ is equal to the difference of the equivalence classes of $x$ and $y$, i.e., $[x - y] = [x] - [y]$.

Submodule.Quotient.forall theorem

{P : M ⧸ p → Prop} : (∀ a, P a) ↔ ∀ a, P (mk a)

Full source

protected nonrec lemma «forall» {P : M ⧸ p → Prop} : (∀ a, P a) ↔ ∀ a, P (mk a) := Quotient.forall

Universal Quantification on Quotient Module via Representatives

Informal description

For any predicate $P$ on the quotient module $M ⧸ p$, the statement $(\forall a \in M ⧸ p, P(a))$ holds if and only if for all $a \in M$, $P([a])$ holds, where $[a]$ denotes the equivalence class of $a$ in $M ⧸ p$.

Submodule.Quotient.subsingleton_iff theorem

: Subsingleton (M ⧸ p) ↔ ∀ x : M, x ∈ p

Full source

theorem subsingleton_iff : SubsingletonSubsingleton (M ⧸ p) ↔ ∀ x : M, x ∈ p := by
  rw [subsingleton_iff_forall_eq 0, Submodule.Quotient.forall]
  simp_rw [Submodule.Quotient.mk_eq_zero]

Quotient Module is Subsingleton iff Submodule is Entire Module

Informal description

The quotient module $M ⧸ p$ is a subsingleton (i.e., has at most one element) if and only if every element $x$ of $M$ belongs to the submodule $p$.

Submodule.Quotient.instSMul' instance

: SMul S (M ⧸ P)

Full source

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)⟩

Scalar Multiplication on Quotient Modules

Informal description

For any module $M$ over a ring $R$ with a submodule $P$, and any scalar action of a type $S$ on $M$, the quotient module $M ⧸ P$ inherits a scalar multiplication operation from $S$.

Submodule.Quotient.instSMul instance

: SMul R (M ⧸ P)

Full source

/-- Shortcut to help the elaborator in the common case. -/
instance instSMul : SMul R (M ⧸ P) :=
  Quotient.instSMul' P

Scalar Multiplication on Quotient Modules by the Base Ring

Informal description

For any module $M$ over a ring $R$ with a submodule $P$, the quotient module $M ⧸ P$ inherits a scalar multiplication operation from $R$.

Submodule.Quotient.mk_smul theorem

(r : S) (x : M) : (mk (r • x) : M ⧸ p) = r • mk x

Full source

@[simp]
theorem mk_smul (r : S) (x : M) : (mk (r • x) : M ⧸ p) = r • mk x :=
  rfl

Scalar Multiplication Commutes with Quotient Map: $[r \cdot x] = r \cdot [x]$

Informal description

For any scalar $r$ in $S$ and any element $x$ in a module $M$ over a ring $R$, the equivalence class of $r \cdot x$ in the quotient module $M ⧸ p$ is equal to $r$ times the equivalence class of $x$, i.e., $[r \cdot x] = r \cdot [x]$.

Submodule.Quotient.smulCommClass instance

(T : Type*) [SMul T R] [SMul T M] [IsScalarTower T R M] [SMulCommClass S T M] : SMulCommClass S T (M ⧸ P)

Full source

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 _ _ _)

Commutativity of Scalar Actions on Quotient Modules

Informal description

For any module $M$ over a ring $R$ with a submodule $P$, and any scalar actions of types $S$ and $T$ on $M$ such that: 1. $T$ acts on $R$ and $M$ compatibly via the `IsScalarTower` condition, 2. The actions of $S$ and $T$ on $M$ commute (i.e., $s \cdot (t \cdot m) = t \cdot (s \cdot m)$ for all $s \in S$, $t \in T$, $m \in M$), then the actions of $S$ and $T$ also commute on the quotient module $M ⧸ P$.

Submodule.Quotient.isScalarTower instance

(T : Type*) [SMul T R] [SMul T M] [IsScalarTower T R M] [SMul S T] [IsScalarTower S T M] : IsScalarTower S T (M ⧸ P)

Full source

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 _ _ _)

Scalar Tower Structure on Quotient Modules

Informal description

For any module $M$ over a ring $R$ with a submodule $P$, and any scalar actions of types $S$ and $T$ on $M$ such that $T$ acts on $R$ and the actions are compatible via the tower condition $S \to T \to R \to M$, the quotient module $M ⧸ P$ inherits a scalar tower structure from $S$ to $T$ to $M ⧸ P$.

Submodule.Quotient.isCentralScalar instance

 [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M] : IsCentralScalar S (M ⧸ P)

Full source

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 _ _

Central Scalar Multiplication on Quotient Modules

Informal description

For any module $M$ over a ring $R$ with a submodule $P$, and any scalar action of a type $S$ on $M$ that is central (i.e., the left and right scalar actions coincide), the quotient module $M ⧸ P$ inherits a central scalar multiplication operation from $S$.

Submodule.Quotient.mulAction' instance

[Monoid S] [SMul S R] [MulAction S M] [IsScalarTower S R M] (P : Submodule R M) : MulAction S (M ⧸ P)

Full source

instance mulAction' [Monoid S] [SMul S R] [MulAction S M] [IsScalarTower S R M]
    (P : Submodule R M) : MulAction S (M ⧸ P) := fast_instance%
  Function.Surjective.mulAction mk Quot.mk_surjective <| Submodule.Quotient.mk_smul P

Multiplicative Action on Quotient Modules

Informal description

For any monoid $S$ acting on a module $M$ over a ring $R$ in a way compatible with the scalar multiplication (i.e., $S$ acts on $R$ and $M$ such that the actions are compatible via the `IsScalarTower` condition), and for any submodule $P$ of $M$, the quotient module $M ⧸ P$ inherits a multiplicative action from $S$.

Submodule.Quotient.mulAction instance

(P : Submodule R M) : MulAction R (M ⧸ P)

Full source

instance mulAction (P : Submodule R M) : MulAction R (M ⧸ P) :=
  Quotient.mulAction' P

Multiplicative Action on Quotient Modules by the Base Ring

Informal description

For any module $M$ over a ring $R$ and any submodule $P$ of $M$, the quotient module $M ⧸ P$ inherits a multiplicative action from $R$.

Submodule.Quotient.smulZeroClass' instance

[SMul S R] [SMulZeroClass S M] [IsScalarTower S R M] (P : Submodule R M) : SMulZeroClass S (M ⧸ P)

Full source

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

Scalar Multiplication Preserves Zero in Quotient Modules

Informal description

For any ring $R$, module $M$ over $R$, and submodule $P$ of $M$, if $S$ is a type with a scalar multiplication action on $R$ and $M$ such that $M$ is a `SMulZeroClass` with respect to $S$ and the actions are compatible via the `IsScalarTower` condition, then the quotient module $M ⧸ P$ inherits a `SMulZeroClass` structure from $S$. This means that scalar multiplication by elements of $S$ on $M ⧸ P$ satisfies $s \cdot 0 = 0$ for all $s \in S$.

Submodule.Quotient.smulZeroClass instance

(P : Submodule R M) : SMulZeroClass R (M ⧸ P)

Full source

instance smulZeroClass (P : Submodule R M) : SMulZeroClass R (M ⧸ P) :=
  Quotient.smulZeroClass' P

Scalar Multiplication Preserves Zero in Quotient Modules

Informal description

For any module $M$ over a ring $R$ and any submodule $P$ of $M$, the quotient module $M ⧸ P$ inherits a scalar multiplication structure from $R$ that preserves the zero element. Specifically, for any $r \in R$ and the zero equivalence class $0 \in M ⧸ P$, we have $r \cdot 0 = 0$.

Submodule.Quotient.distribSMul' instance

[SMul S R] [DistribSMul S M] [IsScalarTower S R M] (P : Submodule R M) : DistribSMul S (M ⧸ P)

Full source

instance distribSMul' [SMul S R] [DistribSMul S M] [IsScalarTower S R M] (P : Submodule R M) :
    DistribSMul S (M ⧸ P) := fast_instance%
  Function.Surjective.distribSMul {toFun := mk, map_zero' := rfl, map_add' := fun _ _ => rfl}
    Quot.mk_surjective (Submodule.Quotient.mk_smul P)

Distributive Scalar Multiplication on Quotient Modules

Informal description

For any ring $R$, module $M$ over $R$, and submodule $P$ of $M$, if $S$ is a type with a scalar multiplication action on $R$ and $M$ such that $M$ is a `DistribSMul` with respect to $S$ and the actions are compatible via the `IsScalarTower` condition, then the quotient module $M ⧸ P$ inherits a `DistribSMul` structure from $S$. This means that scalar multiplication by elements of $S$ on $M ⧸ P$ distributes over addition and zero.

Submodule.Quotient.distribSMul instance

(P : Submodule R M) : DistribSMul R (M ⧸ P)

Full source

instance distribSMul (P : Submodule R M) : DistribSMul R (M ⧸ P) :=
  Quotient.distribSMul' P

Distributive Scalar Multiplication on Quotient Modules

Informal description

For any module $M$ over a ring $R$ and any submodule $P$ of $M$, the quotient module $M ⧸ P$ inherits a distributive scalar multiplication structure from $R$. This means that scalar multiplication by elements of $R$ on $M ⧸ P$ distributes over addition and zero.

Submodule.Quotient.distribMulAction' instance

[Monoid S] [SMul S R] [DistribMulAction S M] [IsScalarTower S R M] (P : Submodule R M) : DistribMulAction S (M ⧸ P)

Full source

instance distribMulAction' [Monoid S] [SMul S R] [DistribMulAction S M] [IsScalarTower S R M]
    (P : Submodule R M) : DistribMulAction S (M ⧸ P) := fast_instance%
  Function.Surjective.distribMulAction {toFun := mk, map_zero' := rfl, map_add' := fun _ _ => rfl}
    Quot.mk_surjective (Submodule.Quotient.mk_smul P)

Distributive Multiplicative Action on Quotient Modules

Informal description

For any monoid $S$ acting on a module $M$ over a ring $R$ in a way compatible with the scalar multiplication (i.e., $S$ acts on $R$ and $M$ such that the actions are compatible via the `IsScalarTower` condition), and for any submodule $P$ of $M$, the quotient module $M ⧸ P$ inherits a distributive multiplicative action from $S$.

Submodule.Quotient.distribMulAction instance

(P : Submodule R M) : DistribMulAction R (M ⧸ P)

Full source

instance distribMulAction (P : Submodule R M) : DistribMulAction R (M ⧸ P) :=
  Quotient.distribMulAction' P

Distributive Multiplicative Action on Quotient Modules by Submodules

Informal description

For any module $M$ over a ring $R$ and any submodule $P$ of $M$, the quotient module $M ⧸ P$ inherits a distributive multiplicative action from $R$.

Submodule.Quotient.module' instance

[Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] (P : Submodule R M) : Module S (M ⧸ P)

Full source

instance module' [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] (P : Submodule R M) :
    Module S (M ⧸ P) := fast_instance%
  Function.Surjective.module _ {toFun := mk, map_zero' := by rfl, map_add' := fun _ _ => by rfl}
    Quot.mk_surjective (Submodule.Quotient.mk_smul P)

Module Structure on Quotient Modules via Compatible Semiring Actions

Informal description

For any semiring $S$ acting on a module $M$ over a ring $R$ in a way compatible with the scalar multiplication (i.e., $S$ acts on $R$ and $M$ such that the actions are compatible via the `IsScalarTower` condition), and for any submodule $P$ of $M$, the quotient module $M ⧸ P$ inherits a module structure over $S$.

Submodule.Quotient.module instance

(P : Submodule R M) : Module R (M ⧸ P)

Full source

instance module (P : Submodule R M) : Module R (M ⧸ P) :=
  Quotient.module' P

Module Structure on Quotient Modules

Informal description

For any module $M$ over a ring $R$ and any submodule $P$ of $M$, the quotient module $M ⧸ P$ inherits a module structure over $R$.

Submodule.Quotient.induction_on theorem

{C : M ⧸ p → Prop} (x : M ⧸ p) (H : ∀ z, C (Submodule.Quotient.mk z)) : C x

Full source

@[elab_as_elim]
theorem induction_on {C : M ⧸ p → Prop} (x : M ⧸ p) (H : ∀ z, C (Submodule.Quotient.mk z)) :
    C x := Quotient.inductionOn' x H

Induction Principle for Quotient Modules

Informal description

For any predicate $C$ on the quotient module $M ⧸ p$ and any element $x \in M ⧸ p$, if $C$ holds for the equivalence class of every element $z \in M$, then $C$ holds for $x$.

Submodule.Quotient.mk_surjective theorem

: Function.Surjective (@mk _ _ _ _ _ p)

Full source

theorem mk_surjective : Function.Surjective (@mk _ _ _ _ _ p) := by
  rintro ⟨x⟩
  exact ⟨x, rfl⟩

Surjectivity of the Quotient Module Map

Informal description

The quotient map $\operatorname{mk} : M \to M ⧸ p$ is surjective, where $M$ is a module over a ring $R$ and $p$ is a submodule of $M$. That is, for every element $[x] \in M ⧸ p$, there exists an element $y \in M$ such that $\operatorname{mk}(y) = [x]$.

Submodule.quot_hom_ext theorem

(f g : (M ⧸ p) →ₗ[R] M₂) (h : ∀ x : M, f (Quotient.mk x) = g (Quotient.mk x)) : f = g

Full source

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 => Submodule.Quotient.induction_on _ x h

Uniqueness of Linear Maps from Quotient Module via Equality on Representatives

Informal description

Let $M$ be a module over a ring $R$, $p$ a submodule of $M$, and $M_2$ another $R$-module. For any two linear maps $f, g: M ⧸ p \to M_2$, if $f([x]) = g([x])$ for all $x \in M$ (where $[x]$ denotes the equivalence class of $x$ in $M ⧸ p$), then $f = g$.

Submodule.mkQ definition

: M →ₗ[R] M ⧸ p

Full source

/-- 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

Quotient module linear map

Informal description

The linear map from a module $M$ over a ring $R$ to the quotient module $M ⧸ p$, where $p$ is a submodule of $M$, sending each element $x \in M$ to its equivalence class $[x] \in M ⧸ p$.

Submodule.mkQ_apply theorem

(x : M) : p.mkQ x = Quotient.mk x

Full source

@[simp]
theorem mkQ_apply (x : M) : p.mkQ x = Quotient.mk x :=
  rfl

Equality of Quotient Map and Equivalence Class Construction

Informal description

For any element $x$ in a module $M$ over a ring $R$, the image of $x$ under the quotient linear map $p.\text{mkQ}$ is equal to the equivalence class of $x$ in the quotient module $M ⧸ p$, i.e., $p.\text{mkQ}(x) = [x]$.

Submodule.mkQ_surjective theorem

: Function.Surjective p.mkQ

Full source

theorem mkQ_surjective : Function.Surjective p.mkQ := by
  rintro ⟨x⟩; exact ⟨x, rfl⟩

Surjectivity of the Quotient Module Map $\operatorname{mkQ}$

Informal description

The canonical linear map $\operatorname{mkQ} : M \to M ⧸ p$ from a module $M$ to its quotient module by a submodule $p$ is surjective. That is, for every element $[x] \in M ⧸ p$, there exists an element $y \in M$ such that $\operatorname{mkQ}(y) = [x]$.

Submodule.linearMap_qext theorem

⦃f g : M ⧸ p →ₛₗ[τ₁₂] M₂⦄ (h : f.comp p.mkQ = g.comp p.mkQ) : f = g

Full source

/-- 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 ⧸ pM ⧸ p →ₛₗ[τ₁₂] M₂⦄ (h : f.comp p.mkQ = g.comp p.mkQ) : f = g :=
  LinearMap.ext fun x => Submodule.Quotient.induction_on _ x <| (LinearMap.congr_fun h :)

Uniqueness of Linear Maps from Quotient Module via Composition with Quotient Map

Informal description

Let $M$ be a module over a ring $R$, $p$ a submodule of $M$, and $M_2$ another module over $R$ (possibly with a different ring action via $\tau_{12}$). For any two linear maps $f, g: M ⧸ p \to M_2$, if the compositions $f \circ \pi = g \circ \pi$ where $\pi: M \to M ⧸ p$ is the canonical quotient map, then $f = g$.

Submodule.quotEquivOfEq definition

(h : p = p') : (M ⧸ p) ≃ₗ[R] M ⧸ p'

Full source

/-- 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 }

Linear equivalence of quotient modules by equal submodules

Informal description

Given a module $M$ over a ring $R$ and two submodules $p$ and $p'$ of $M$ such that $p = p'$, there exists a linear equivalence between the quotient modules $M ⧸ p$ and $M ⧸ p'$. This equivalence maps each equivalence class $[x]_{p}$ in $M ⧸ p$ to the corresponding equivalence class $[x]_{p'}$ in $M ⧸ p'$.

Submodule.quotEquivOfEq_mk theorem

(h : p = p') (x : M) : Submodule.quotEquivOfEq p p' h (Submodule.Quotient.mk x) = (Submodule.Quotient.mk x)

Full source

@[simp]
theorem quotEquivOfEq_mk (h : p = p') (x : M) :
    Submodule.quotEquivOfEq p p' h (Submodule.Quotient.mk x) =
      (Submodule.Quotient.mk x) :=
  rfl

Equality of Submodules Implies Equality of Quotient Classes

Informal description

Let $M$ be a module over a ring $R$, and let $p$ and $p'$ be submodules of $M$ such that $p = p'$. For any element $x \in M$, the linear equivalence $\text{quotEquivOfEq}$ between the quotient modules $M ⧸ p$ and $M ⧸ p'$ maps the equivalence class $[x]_p$ to $[x]_{p'}$.

Main definitions