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) [Eil76]; 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.

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

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

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

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

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 ([Eil76]).

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.