# Congruence relations respecting scalar multiplication #

source
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.

Instances For

source
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.

Instances For

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

Instances For

source
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

Instances For

source
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

Instances For

source
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) ⋯ }

source
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) ⋯ }

source
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⟧ }

source
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 := ⋯ }

source
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 := ⋯ }

source
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 := ⋯ }

source
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 := ⋯ }

source
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 := ⋯ }

Instances For

source
@[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 ⋯

Instances For

source
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

Instances For

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

source
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⟧ }

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

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

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

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

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

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

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

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

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

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

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

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

source
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 := ⋯ }

source
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 := ⋯ }

source
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 := ⋯ }

source
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 := ⋯ }

Instances For

source
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 := ⋯ }

Instances For

source
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 := ⋯ }

Instances For

source
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.

Instances For