Congruence relations respecting scalar multiplication

structure VAddCon (S : Type u_2) (M : Type u_3) [VAdd S M] extends Setoid M : Type u_3

A congruence relation that preserves additive action.

• r : M → M → Prop
• iseqv : Equivalence ⇑self.toSetoid
• vadd (s : S) {x y : M} : self.toSetoid x y → self.toSetoid (s +ᵥ x) (s +ᵥ y)

  A VAddCon is closed under additive action.

structure SMulCon (S : Type u_2) (M : Type u_3) [SMul S M] extends Setoid M : Type u_3

A congruence relation that preserves scalar multiplication.

• r : M → M → Prop
• iseqv : Equivalence ⇑self.toSetoid
• smul (s : S) {x y : M} : self.toSetoid x y → self.toSetoid (s • x) (s • y)

  A SMulCon is closed under scalar multiplication.

structure ModuleCon (S : Type u_2) (M : Type u_3) [Add M] [SMul S M] extends AddCon M, SMulCon S M : Type u_3

A congruence relation that preserves addition and scalar multiplication. The quotient by a ModuleCon inherits DistribSMul, DistribMulAction, and Module instances.

• r : M → M → Prop
• iseqv : Equivalence ⇑self.toSetoid
• add' {w x y z : M} : self.toSetoid w x → self.toSetoid y z → self.toSetoid (w + y) (x + z)
• smul (s : S) {x y : M} : self.toSetoid x y → self.toSetoid (s • x) (s • y)

def SMulCon.Quotient {S : Type u_2} (M : Type u_3) [SMul S M] (c : SMulCon S M) : Type u_3

The quotient by a congruence relation preserving scalar multiplication.

def VAddCon.Quotient {S : Type u_2} (M : Type u_3) [VAdd S M] (c : VAddCon S M) : Type u_3

The quotient by a congruence relation preserving additive action.

instance SMulCon.instSMulQuotient {S : Type u_2} (M : Type u_3) [SMul S M] (c : SMulCon S M) : SMul S (SMulCon.Quotient M c)

instance VAddCon.instVAddQuotient {S : Type u_2} (M : Type u_3) [VAdd S M] (c : VAddCon S M) : VAdd S (VAddCon.Quotient M c)

instance SMulCon.instZeroQuotient {S : Type u_2} (M : Type u_3) [SMul S M] [Zero M] (c : SMulCon S M) : Zero (SMulCon.Quotient M c)

instance SMulCon.instSMulZeroClassQuotient {S : Type u_2} (M : Type u_3) [Zero M] [SMulZeroClass S M] (c : SMulCon S M) : SMulZeroClass S (SMulCon.Quotient M c)

instance SMulCon.instSMulWithZeroQuotient {S : Type u_2} (M : Type u_3) [Zero S] [Zero M] [SMulWithZero S M] (c : SMulCon S M) : SMulWithZero S (SMulCon.Quotient M c)

instance SMulCon.instMulActionQuotient {S : Type u_2} (M : Type u_3) [Monoid S] [MulAction S M] (c : SMulCon S M) : MulAction S (SMulCon.Quotient M c)

instance VAddCon.instAddActionQuotient {S : Type u_2} (M : Type u_3) [AddMonoid S] [AddAction S M] (c : VAddCon S M) : AddAction S (VAddCon.Quotient M c)

def SMulCon.addConGen' {S : Type u_2} {M : Type u_3} [AddZeroClass M] [DistribSMul S M] (r : M → M → Prop) (hr : ∀ (s : S) {m m' : M}, r m m' → r (s • m) (s • m')) : ModuleCon S M

The AddCon generated by a relation respecting scalar multiplication is a ModuleCon.

@[reducible, inline]

abbrev SMulCon.addConGen {S : Type u_2} {M : Type u_3} [AddZeroClass M] [DistribSMul S M] (c : SMulCon S M) : ModuleCon S M

The AddCon generated by a SMulCon is a ModuleCon.

def ModuleCon.Quotient {S : Type u_2} (M : Type u_3) [Add M] [SMul S M] (c : ModuleCon S M) : Type u_3

The quotient by a congruence relation preserving addition and scalar multiplication.

instance ModuleCon.instSMulQuotient {S : Type u_2} (M : Type u_3) [SMul S M] [Add M] (c : ModuleCon S M) : SMul S (ModuleCon.Quotient M c)

instance ModuleCon.instZeroQuotient {S : Type u_2} (M : Type u_3) [SMul S M] [Zero M] [Add M] (c : ModuleCon S M) : Zero (ModuleCon.Quotient M c)

instance ModuleCon.instAddQuotient {S : Type u_2} (M : Type u_3) [SMul S M] [Add M] (c : ModuleCon S M) : Add (ModuleCon.Quotient M c)

instance ModuleCon.instAddZeroClassQuotient {S : Type u_2} (M : Type u_3) [SMul S M] [AddZeroClass M] (c : ModuleCon S M) : AddZeroClass (ModuleCon.Quotient M c)

instance ModuleCon.instAddCommMagmaQuotient {S : Type u_2} (M : Type u_3) [SMul S M] [AddCommMagma M] (c : ModuleCon S M) : AddCommMagma (ModuleCon.Quotient M c)

instance ModuleCon.instAddSemigroupQuotient {S : Type u_2} (M : Type u_3) [SMul S M] [AddSemigroup M] (c : ModuleCon S M) : AddSemigroup (ModuleCon.Quotient M c)

instance ModuleCon.instAddCommSemigroupQuotient {S : Type u_2} (M : Type u_3) [SMul S M] [AddCommSemigroup M] (c : ModuleCon S M) : AddCommSemigroup (ModuleCon.Quotient M c)

instance ModuleCon.instAddMonoidQuotient {S : Type u_2} (M : Type u_3) [SMul S M] [AddMonoid M] (c : ModuleCon S M) : AddMonoid (ModuleCon.Quotient M c)

instance ModuleCon.instAddCommMonoidQuotient {S : Type u_2} (M : Type u_3) [SMul S M] [AddCommMonoid M] (c : ModuleCon S M) : AddCommMonoid (ModuleCon.Quotient M c)

instance ModuleCon.instAddGroupQuotient {S : Type u_2} (M : Type u_3) [SMul S M] [AddGroup M] (c : ModuleCon S M) : AddGroup (ModuleCon.Quotient M c)

instance ModuleCon.instAddCommGroupQuotient {S : Type u_2} (M : Type u_3) [SMul S M] [AddCommGroup M] (c : ModuleCon S M) : AddCommGroup (ModuleCon.Quotient M c)

instance ModuleCon.instSMulZeroClassQuotient {S : Type u_2} (M : Type u_3) [Zero M] [Add M] [SMulZeroClass S M] (c : ModuleCon S M) : SMulZeroClass S (ModuleCon.Quotient M c)

instance ModuleCon.instSMulWithZeroQuotient {S : Type u_2} (M : Type u_3) [Zero S] [Zero M] [Add M] [SMulWithZero S M] (c : ModuleCon S M) : SMulWithZero S (ModuleCon.Quotient M c)

instance ModuleCon.instMulActionQuotient {S : Type u_2} (M : Type u_3) [Monoid S] [Add M] [MulAction S M] (c : ModuleCon S M) : MulAction S (ModuleCon.Quotient M c)

instance ModuleCon.instDistribSMulQuotient {S : Type u_2} (M : Type u_3) [AddZeroClass M] [DistribSMul S M] (c : ModuleCon S M) : DistribSMul S (ModuleCon.Quotient M c)

instance ModuleCon.instDistribMulActionQuotient {S : Type u_2} (M : Type u_3) [Monoid S] [AddMonoid M] [DistribMulAction S M] (c : ModuleCon S M) : DistribMulAction S (ModuleCon.Quotient M c)

instance ModuleCon.instModuleQuotient {S : Type u_2} (M : Type u_3) [Semiring S] [AddCommMonoid M] [Module S M] (c : ModuleCon S M) : Module S (ModuleCon.Quotient M c)

def SMulCon.ker {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [SMul R M] [SMul S N] {φ : R → S} (f : M →ₑ[φ] N) : SMulCon R M

The kernel of a MulActionHom as a congruence relation.

def VAddCon.ker {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [VAdd R M] [VAdd S N] {φ : R → S} (f : M →ₑ[φ] N) : VAddCon R M

The kernel of an AddActionHom as a congruence relation.

def ModuleCon.ker {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Monoid R] [Monoid S] [AddMonoid M] [AddMonoid N] [DistribMulAction R M] [DistribMulAction S N] {φ : R →* S} (f : M →ₑ+[φ] N) : ModuleCon R M

The kernel of a DistribMulActionHom as a congruence relation.

noncomputable def ModuleCon.quotientKerEquivOfSurjective {S : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module S M] [Module S N] (f : M →ₗ[S] N) (hf : Function.Surjective ⇑f) : ModuleCon.Quotient M (ker f.toDistribMulActionHom) ≃ₗ[S] N

The first isomorphism theorem for semimodules in the case of a surjective homomorphism.