Documentation

Linglib.Core.Algebra.Group.Subquotient

Subquotients of monoids #

A monoid T is a subquotient of a monoid S when T is a homomorphic image of a submonoid of S. In finite semigroup theory the relation is called division (T ≼ S), and in group theory a section. This file defines the relation and proves it transitive, closed under products, and, on finite monoids, antisymmetric up to isomorphism.

Main definitions #

Monoid.IsSubquotient T S: T is a homomorphic image of a submonoid of S.

References #

[Eil76]

def Monoid.IsSubquotient (T : Type u_4) (S : Type u_5) [Monoid T] [Monoid S] :

A monoid T is a subquotient of S when it is a homomorphic image of a submonoid of S.

Equations

Monoid.IsSubquotient T S = ∃ (N : Submonoid S) (f : ↥N →* T), Function.Surjective ⇑f

Instances For

def AddMonoid.IsSubquotient (T : Type u_4) (S : Type u_5) [AddMonoid T] [AddMonoid S] :

An additive monoid T is a subquotient of S when it is a homomorphic image of an additive submonoid of S.

Equations

AddMonoid.IsSubquotient T S = ∃ (N : AddSubmonoid S) (f : ↥N →+ T), Function.Surjective ⇑f

Instances For

theorem Monoid.IsSubquotient.of_surjective {T : Type u_1} {S : Type u_2} [Monoid T] [Monoid S] (f : S →* T) (hf : Function.Surjective ⇑f) :

IsSubquotient T S

theorem AddMonoid.IsSubquotient.of_surjective {T : Type u_1} {S : Type u_2} [AddMonoid T] [AddMonoid S] (f : S →+ T) (hf : Function.Surjective ⇑f) :

IsSubquotient T S

theorem MulEquiv.isSubquotient {T : Type u_1} {S : Type u_2} [Monoid T] [Monoid S] (e : T ≃* S) :

Monoid.IsSubquotient T S

theorem AddEquiv.isSubquotient {T : Type u_1} {S : Type u_2} [AddMonoid T] [AddMonoid S] (e : T ≃+ S) :

AddMonoid.IsSubquotient T S

theorem Monoid.IsSubquotient.refl (T : Type u_4) [Monoid T] :

IsSubquotient T T

theorem AddMonoid.IsSubquotient.refl (T : Type u_4) [AddMonoid T] :

IsSubquotient T T

theorem Submonoid.isSubquotient {S : Type u_2} [Monoid S] (N : Submonoid S) :

Monoid.IsSubquotient (↥N) S

theorem AddSubmonoid.isSubquotient {S : Type u_2} [AddMonoid S] (N : AddSubmonoid S) :

AddMonoid.IsSubquotient (↥N) S

theorem Con.isSubquotient_quotient {S : Type u_2} [Monoid S] (c : Con S) :

Monoid.IsSubquotient c.Quotient S

theorem AddCon.isSubquotient_quotient {S : Type u_2} [AddMonoid S] (c : AddCon S) :

AddMonoid.IsSubquotient c.Quotient S

theorem MonoidHom.isSubquotient_mrange {T : Type u_1} {S : Type u_2} [Monoid T] [Monoid S] (f : S →* T) :

Monoid.IsSubquotient (↥(mrange f)) S

theorem AddMonoidHom.isSubquotient_mrange {T : Type u_1} {S : Type u_2} [AddMonoid T] [AddMonoid S] (f : S →+ T) :

AddMonoid.IsSubquotient (↥(mrange f)) S

theorem Monoid.IsSubquotient.trans {T : Type u_1} {S : Type u_2} {R : Type u_3} [Monoid T] [Monoid S] [Monoid R] (hTS : IsSubquotient T S) (hSR : IsSubquotient S R) :

IsSubquotient T R

theorem AddMonoid.IsSubquotient.trans {T : Type u_1} {S : Type u_2} {R : Type u_3} [AddMonoid T] [AddMonoid S] [AddMonoid R] (hTS : IsSubquotient T S) (hSR : IsSubquotient S R) :

IsSubquotient T R

theorem Monoid.IsSubquotient.of_injective {T : Type u_1} {S : Type u_2} [Monoid T] [Monoid S] (f : T →* S) (hf : Function.Injective ⇑f) :

IsSubquotient T S

theorem AddMonoid.IsSubquotient.of_injective {T : Type u_1} {S : Type u_2} [AddMonoid T] [AddMonoid S] (f : T →+ S) (hf : Function.Injective ⇑f) :

IsSubquotient T S

theorem Monoid.isSubquotient_prod_left (T : Type u_4) (S : Type u_5) [Monoid T] [Monoid S] :

IsSubquotient T (T × S)

theorem AddMonoid.isSubquotient_prod_left (T : Type u_4) (S : Type u_5) [AddMonoid T] [AddMonoid S] :

IsSubquotient T (T × S)

theorem Monoid.isSubquotient_prod_right (T : Type u_4) (S : Type u_5) [Monoid T] [Monoid S] :

IsSubquotient T (S × T)

theorem AddMonoid.isSubquotient_prod_right (T : Type u_4) (S : Type u_5) [AddMonoid T] [AddMonoid S] :

IsSubquotient T (S × T)

theorem Monoid.IsSubquotient.prod {T : Type u_1} {S : Type u_2} [Monoid T] [Monoid S] {T' : Type u_4} {S' : Type u_5} [Monoid T'] [Monoid S'] (h : IsSubquotient T S) (h' : IsSubquotient T' S') :

IsSubquotient (T × T') (S × S')

Subquotients are closed under componentwise products.

theorem AddMonoid.IsSubquotient.prod {T : Type u_1} {S : Type u_2} [AddMonoid T] [AddMonoid S] {T' : Type u_4} {S' : Type u_5} [AddMonoid T'] [AddMonoid S'] (h : IsSubquotient T S) (h' : IsSubquotient T' S') :

IsSubquotient (T × T') (S × S')

Subquotients are closed under componentwise products.

theorem Monoid.IsSubquotient.finite {T : Type u_1} {S : Type u_2} [Monoid T] [Monoid S] [Finite S] (h : IsSubquotient T S) :

Finite T

theorem AddMonoid.IsSubquotient.finite {T : Type u_1} {S : Type u_2} [AddMonoid T] [AddMonoid S] [Finite S] (h : IsSubquotient T S) :

Finite T

theorem Monoid.IsSubquotient.card_le {T : Type u_1} {S : Type u_2} [Monoid T] [Monoid S] [Finite S] (h : IsSubquotient T S) :

Nat.card T ≤ Nat.card S

theorem AddMonoid.IsSubquotient.card_le {T : Type u_1} {S : Type u_2} [AddMonoid T] [AddMonoid S] [Finite S] (h : IsSubquotient T S) :

Nat.card T ≤ Nat.card S

theorem Monoid.IsSubquotient.nonempty_mulEquiv_of_card_le {T : Type u_1} {S : Type u_2} [Monoid T] [Monoid S] [Finite S] (hTS : IsSubquotient T S) (hle : Nat.card S ≤ Nat.card T) :

Nonempty (T ≃* S)

A subquotient of maximal cardinality is an isomorph.

theorem AddMonoid.IsSubquotient.nonempty_addEquiv_of_card_le {T : Type u_1} {S : Type u_2} [AddMonoid T] [AddMonoid S] [Finite S] (hTS : IsSubquotient T S) (hle : Nat.card S ≤ Nat.card T) :

Nonempty (T ≃+ S)

A subquotient of maximal cardinality is an isomorph.

theorem Monoid.IsSubquotient.nonempty_mulEquiv {T : Type u_1} {S : Type u_2} [Monoid T] [Monoid S] [Finite S] (hTS : IsSubquotient T S) (hST : IsSubquotient S T) :

Nonempty (T ≃* S)

Finite monoids that are subquotients of each other are isomorphic.

theorem AddMonoid.IsSubquotient.nonempty_addEquiv {T : Type u_1} {S : Type u_2} [AddMonoid T] [AddMonoid S] [Finite S] (hTS : IsSubquotient T S) (hST : IsSubquotient S T) :

Nonempty (T ≃+ S)

Finite additive monoids that are subquotients of each other are isomorphic.