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.

Equations

• SMulCon.Quotient M c = Quotient c.toSetoid

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.

Equations

• VAddCon.Quotient M c = Quotient c.toSetoid

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

Equations

• SMulCon.instSMulQuotient M c = { smul := fun (s : S) => Quotient.map (fun (x : M) => s • x) ⋯ }

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

Equations

• VAddCon.instVAddQuotient M c = { vadd := fun (s : S) => Quotient.map (fun (x : M) => s +ᵥ x) ⋯ }

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)

Equations

• SMulCon.instZeroQuotient M c = { zero := ⟦0⟧ }

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)

Equations

• SMulCon.instSMulZeroClassQuotient M c = { toSMul := SMulCon.instSMulQuotient M c, smul_zero := ⋯ }

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)

Equations

• SMulCon.instSMulWithZeroQuotient M c = { toSMulZeroClass := SMulCon.instSMulZeroClassQuotient M c, zero_smul := ⋯ }

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)

Equations

• SMulCon.instMulActionQuotient M c = { toSMul := SMulCon.instSMulQuotient M c, one_smul := ⋯, mul_smul := ⋯ }

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)

Equations

• VAddCon.instAddActionQuotient M c = { toVAdd := VAddCon.instVAddQuotient M c, zero_vadd := ⋯, add_vadd := ⋯ }

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.

Equations

• SMulCon.addConGen' r hr = { toAddCon := addConGen r, smul := ⋯ }

@[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.

Equations

• c.addConGen = SMulCon.addConGen' ⇑c.toSetoid ⋯

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.

Equations

• ModuleCon.Quotient M c = Quotient c.toSetoid

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)

Equations

• ModuleCon.instSMulQuotient M c = inferInstanceAs (SMul S (SMulCon.Quotient M c.toSMulCon))

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)

Equations

• ModuleCon.instZeroQuotient M c = { zero := ⟦0⟧ }

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)

Equations

• ModuleCon.instAddQuotient M c = inferInstanceAs (Add c.Quotient)

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)

Equations

• ModuleCon.instAddZeroClassQuotient M c = inferInstanceAs (AddZeroClass c.Quotient)

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)

Equations

• ModuleCon.instAddCommMagmaQuotient M c = inferInstanceAs (AddCommMagma c.Quotient)

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)

Equations

• ModuleCon.instAddSemigroupQuotient M c = inferInstanceAs (AddSemigroup c.Quotient)

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)

Equations

• ModuleCon.instAddCommSemigroupQuotient M c = inferInstanceAs (AddCommSemigroup c.Quotient)

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)

Equations

• ModuleCon.instAddMonoidQuotient M c = inferInstanceAs (AddMonoid c.Quotient)

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)

Equations

• ModuleCon.instAddCommMonoidQuotient M c = inferInstanceAs (AddCommMonoid c.Quotient)

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)

Equations

• ModuleCon.instAddGroupQuotient M c = inferInstanceAs (AddGroup c.Quotient)

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)

Equations

• ModuleCon.instAddCommGroupQuotient M c = inferInstanceAs (AddCommGroup c.Quotient)

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)

Equations

• ModuleCon.instSMulZeroClassQuotient M c = inferInstanceAs (SMulZeroClass S (SMulCon.Quotient M c.toSMulCon))

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)

Equations

• ModuleCon.instSMulWithZeroQuotient M c = inferInstanceAs (SMulWithZero S (SMulCon.Quotient M c.toSMulCon))

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)

Equations

• ModuleCon.instMulActionQuotient M c = inferInstanceAs (MulAction S (SMulCon.Quotient M c.toSMulCon))

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)

Equations

• ModuleCon.instDistribSMulQuotient M c = { toSMulZeroClass := ModuleCon.instSMulZeroClassQuotient M c, smul_add := ⋯ }

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)

Equations

• ModuleCon.instDistribMulActionQuotient M c = { toMulAction := ModuleCon.instMulActionQuotient M c, smul_zero := ⋯, smul_add := ⋯ }

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)

Equations

• ModuleCon.instModuleQuotient M c = { toDistribMulAction := ModuleCon.instDistribMulActionQuotient M c, add_smul := ⋯, zero_smul := ⋯ }

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.

Equations

• SMulCon.ker f = { toSetoid := Setoid.ker ⇑f, smul := ⋯ }

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.

Equations

• VAddCon.ker f = { toSetoid := Setoid.ker ⇑f, vadd := ⋯ }

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.

Equations

• ModuleCon.ker f = { toSetoid := (SMulCon.ker f.toMulActionHom).toSetoid, add' := ⋯, smul := ⋯ }

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.

Equations

• One or more equations did not get rendered due to their size.