Substructures of Semigroups

In this file, we extend Mathlib's Subsemigroup structure to define structures for Submonoid and Subgroup. Note that these are different that the mathlib notions of Submonoid and Subgroup which requrire the outer structure to also be a monoid/group, so we put all definitions in the Semigroup namespace to avoid conflict

Main Definitions

• Semigroup.Subsemigroup
• Semigroup.Subsemigroup.toSemigroup The semigroup instance on the subtype of a subsemigroup
• Semigroup.Submonoid
• Semigroup.Submonoid.toMonoid The Monoid instance on the subtype of a submonoid
• Semigroup.Subgroup
• Semigroup.Subgroup.toGroup The Group instance on the subtype of a submonoid
• Semigroup.Subgroup.isMaximal A maximal subgroup is a subgroup that is not properly contained in any other subgroup.
• Semigroup.hom_of_bijOn - Noncomputably lift a bijection on the carriers of two subgroups that maps multiplication to an isomorphism between the groups.

References

See https://avigad.github.io/mathematics_in_lean/C08_Hierarchies.html#sub-objects

TODO

Redefine group with only left inverse requirement not both.

Blueprint

Subgroup of a Semigroup Label: def:subgroup-of-semigroup Lean definition to tag: Semigroup.Subgroup dependencies: None

Maximal Subgroup label: def:maximal-subgroup Lean definition to tag: Semigroup.Subgroup.isMaximal Dependencies: def:subgroup-of-semigroup

Structure definitions

The definition of Semigroup.Subsemigroup is copied from mathlibs Subsemigroup, except we requrie an outer Semigroup structure. These BUNDLED structures come with SetLike instances, enabiling a coersion to Set so you can write things like x ∈ H for x : S and H : Subsemigroup S. It also provides the lattice strucure (⊓ ⊔ ⊤ ⊥) and the cannonical subtype H : Type := {x // x ∈ carrier}

structure Semigroup.Subsemigroup (S : Type u_1) [Semigroup S] : Type u_1

A subsemigroup of a Semigroup S is a subset closed under multiplication.

• carrier : Set S

  The carrier of a subsemigroup.

• mul_mem {a b : S} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier

  The product of two elements of a subsemigroup belongs to the subsemigroup.

instance Semigroup.Subsemigroup.instSetLike {S : Type u_1} [Semigroup S] : SetLike (Subsemigroup S) S

We prove that Subsemigroup S has an injective coersion to Set S

Equations

• Semigroup.Subsemigroup.instSetLike = { coe := Semigroup.Subsemigroup.carrier, coe_injective' := ⋯ }

instance Semigroup.Subsemigroup.instMulSubtypeMem {S : Type u_1} [Semigroup S] (T : Subsemigroup S) : Mul ↥T

We define * on the subsemigroup as a subtype

Equations

• T.instMulSubtypeMem = { mul := fun (a b : ↥T) => ⟨↑a * ↑b, ⋯⟩ }

We relate our defintion of * in the subtype to that outside of the subtype

@[simp]

theorem Semigroup.Subsemigroup.coe_mul {S : Type u_1} [Semigroup S] {T : Subsemigroup S} (x y : ↥T) : ↑(x * y) = ↑x * ↑y

@[simp]

theorem Semigroup.Subsemigroup.mk_mul_mk {S : Type u_1} [Semigroup S] {T : Subsemigroup S} (x y : S) (hx : x ∈ T) (hy : y ∈ T) : ⟨x, hx⟩ * ⟨y, hy⟩ = ⟨x * y, ⋯⟩

@[simp]

theorem Semigroup.Subsemigroup.mul_def {S : Type u_1} [Semigroup S] {T : Subsemigroup S} (x y : ↥T) : x * y = ⟨↑x * ↑y, ⋯⟩

instance Semigroup.Subsemigroup.toSemigroup {S : Type u_1} [Semigroup S] {T : Subsemigroup S} : Semigroup ↥T

A subsemigroup is a semigroup on its subtype

Equations

• Semigroup.Subsemigroup.toSemigroup = { toMul := T.instMulSubtypeMem, mul_assoc := ⋯ }

structure Semigroup.Submonoid (S : Type u_1) [Semigroup S] extends Semigroup.Subsemigroup S : Type u_1

A submonoid of a Semigroup S is a subset closed under multiplication and containing and identity element

• carrier : Set S
• mul_mem {a b : S} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one : S

  The one element

• one_mem : self.one ∈ self.carrier

  The one element is in the carrier

• one_mul (x : S) : x ∈ self.carrier → self.one * x = x

  The one element is a left identity in the carrier

• mul_one (x : S) : x ∈ self.carrier → x * self.one = x

  The one element is a right identity in the carrier

theorem Semigroup.Submonoid.one_eq {S : Type u_1} [Semigroup S] {T₁ T₂ : Submonoid S} (heq : T₁.carrier = T₂.carrier) : T₁.one = T₂.one

In Order to obtain the SetLike instance, we need to construct an injection from Submonoids to Sets. This means that we must prove that, if the carrier of two Submonoids is equal, then the one elements must be equal.

instance Semigroup.Submonoid.instSetLike {S : Type u_1} [Semigroup S] : SetLike (Submonoid S) S

We prove that Submonoid S has an injective coersion to Set S

Equations

• Semigroup.Submonoid.instSetLike = { coe := Semigroup.Subsemigroup.carrier ∘ Semigroup.Submonoid.toSubsemigroup, coe_injective' := ⋯ }

instance Semigroup.Submonoid.instMulSubtypeMem {S : Type u_1} [Semigroup S] (T : Submonoid S) : Mul ↥T

We define * on the submonoid as a subtype

Equations

• T.instMulSubtypeMem = { mul := fun (a b : ↥T) => ⟨↑a * ↑b, ⋯⟩ }

We relate our defintion of * in the subtype to that outside of the subtype

@[simp]

theorem Semigroup.Submonoid.coe_mul {S : Type u_1} [Semigroup S] {T : Submonoid S} (x y : ↥T) : ↑(x * y) = ↑x * ↑y

@[simp]

theorem Semigroup.Submonoid.mk_mul_mk {S : Type u_1} [Semigroup S] {T : Submonoid S} (x y : S) (hx : x ∈ T) (hy : y ∈ T) : ⟨x, hx⟩ * ⟨y, hy⟩ = ⟨x * y, ⋯⟩

@[simp]

theorem Semigroup.Submonoid.mul_def {S : Type u_1} [Semigroup S] {T : Submonoid S} (x y : ↥T) : x * y = ⟨↑x * ↑y, ⋯⟩

instance Semigroup.Submonoid.instSubtypeMem {S : Type u_1} [Semigroup S] {T : Submonoid S} : Semigroup ↥T

Equations

• Semigroup.Submonoid.instSubtypeMem = { toMul := T.instMulSubtypeMem, mul_assoc := ⋯ }

instance Semigroup.Submonoid.instOneSubtypeMem {S : Type u_1} [Semigroup S] {T : Submonoid S} : One ↥T

Equations

• Semigroup.Submonoid.instOneSubtypeMem = { one := ⟨T.one, ⋯⟩ }

We relate our identiy properties to the subtype

theorem Semigroup.Submonoid.one_def {S : Type u_1} [Semigroup S] {T : Submonoid S} : 1 = ⟨T.one, ⋯⟩

@[simp]

theorem Semigroup.Submonoid.coe_one {S : Type u_1} [Semigroup S] {T : Submonoid S} : ↑1 = T.one

@[simp]

theorem Semigroup.Submonoid.coe_mul_one {S : Type u_1} [Semigroup S] {T : Submonoid S} (x : ↥T) : x * 1 = x

@[simp]

theorem Semigroup.Submonoid.coe_one_mul {S : Type u_1} [Semigroup S] {T : Submonoid S} (x : ↥T) : 1 * x = x

instance Semigroup.Submonoid.toMonoid {S : Type u_1} [Semigroup S] {T : Submonoid S} : Monoid ↥T

A Submonoid is a Monoid on its subtype

Equations

• Semigroup.Submonoid.toMonoid = { toMul := T.instMulSubtypeMem, mul_assoc := ⋯, one := ⟨T.one, ⋯⟩, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯ }

structure Semigroup.Subgroup (S : Type u_1) [Semigroup S] extends Semigroup.Submonoid S : Type u_1

A Subgroup of a Semigroup S is a subset closed under multiplication and containing and identity element and an inverse function

• carrier : Set S
• mul_mem {a b : S} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one : S
• one_mem : self.one ∈ self.carrier
• one_mul (x : S) : x ∈ self.carrier → self.one * x = x
• mul_one (x : S) : x ∈ self.carrier → x * self.one = x
• inv (x : S) : S

  The inverse function

• inv_not_mem {x : S} (hin : x ∉ self.carrier) : self.inv x = x

  The inverse function is the identity if x ∉ carrier. This is to ensure injectivity with Set

• inv_mem {x : S} (hin : x ∈ self.carrier) : self.inv x ∈ self.carrier

  The inverses are in the carrier

• inv_mul {x : S} (hin : x ∈ self.carrier) : self.inv x * x = self.one

  The inverse function provides right inverses

• mul_inv {x : S} (hin : x ∈ self.carrier) : x * self.inv x = self.one

  The inverse function provides left inverses

theorem Semigroup.Subgroup.one_eq {S : Type u_1} [Semigroup S] {T₁ T₂ : Subgroup S} (heq : T₁.carrier = T₂.carrier) : T₁.one = T₂.one

In Order to obtain the SetLike instance, we need to construct an injection from Subgroups to Sets. This means that we must prove that, if the carrier of two Submonoids is equal, then the one elements and the inverse functions must be equal.

theorem Semigroup.Subgroup.inv_unique' {S : Type u_1} [Semigroup S] {T : Subgroup S} {x y : S} (hx : x ∈ T.carrier) (hy : y ∈ T.carrier) (heq : T.one = x * y) : T.inv y = x

theorem Semigroup.Subgroup.inv_unique {S : Type u_1} [Semigroup S] {T : Subgroup S} {x y : S} (hx : x ∈ T.carrier) (hy : y ∈ T.carrier) (heq : T.one = x * y) : T.inv x = y

theorem Semigroup.Subgroup.inv_eq {S : Type u_1} [Semigroup S] {T₁ T₂ : Subgroup S} (heq : T₁.carrier = T₂.carrier) : T₁.inv = T₂.inv

instance Semigroup.Subgroup.instSetLike {S : Type u_1} [Semigroup S] : SetLike (Subgroup S) S

We prove that Subgroup S has an injective coersion to Set S

Equations

• Semigroup.Subgroup.instSetLike = { coe := Semigroup.Subsemigroup.carrier ∘ Semigroup.Submonoid.toSubsemigroup ∘ Semigroup.Subgroup.toSubmonoid, coe_injective' := ⋯ }

instance Semigroup.Subgroup.instMulSubtypeMem {S : Type u_1} [Semigroup S] (T : Subgroup S) : Mul ↥T

We define * on the submonoid as a subtype

Equations

• T.instMulSubtypeMem = { mul := fun (a b : ↥T) => ⟨↑a * ↑b, ⋯⟩ }

We relate our defintion of * in the subtype to that outside of the subtype

@[simp]

theorem Semigroup.Subgroup.coe_mul {S : Type u_1} [Semigroup S] {T : Subgroup S} (x y : ↥T) : ↑(x * y) = ↑x * ↑y

@[simp]

theorem Semigroup.Subgroup.mk_mul_mk {S : Type u_1} [Semigroup S] {T : Subgroup S} (x y : S) (hx : x ∈ T) (hy : y ∈ T) : ⟨x, hx⟩ * ⟨y, hy⟩ = ⟨x * y, ⋯⟩

@[simp]

theorem Semigroup.Subgroup.mul_def {S : Type u_1} [Semigroup S] {T : Subgroup S} (x y : ↥T) : x * y = ⟨↑x * ↑y, ⋯⟩

instance Semigroup.Subgroup.instSubtypeMem {S : Type u_1} [Semigroup S] {T : Subgroup S} : Semigroup ↥T

Equations

• Semigroup.Subgroup.instSubtypeMem = { toMul := T.instMulSubtypeMem, mul_assoc := ⋯ }

instance Semigroup.Subgroup.instOneSubtypeMem {S : Type u_1} [Semigroup S] {T : Subgroup S} : One ↥T

Equations

• Semigroup.Subgroup.instOneSubtypeMem = { one := ⟨T.one, ⋯⟩ }

We relate our identiy properties to the subtype

theorem Semigroup.Subgroup.one_def {S : Type u_1} [Semigroup S] {T : Subgroup S} : 1 = ⟨T.one, ⋯⟩

@[simp]

theorem Semigroup.Subgroup.coe_one {S : Type u_1} [Semigroup S] {T : Subgroup S} : ↑1 = T.one

@[simp]

theorem Semigroup.Subgroup.coe_mul_one {S : Type u_1} [Semigroup S] {T : Subgroup S} (x : ↥T) : x * 1 = x

@[simp]

theorem Semigroup.Subgroup.coe_one_mul {S : Type u_1} [Semigroup S] {T : Subgroup S} (x : ↥T) : 1 * x = x

instance Semigroup.Subgroup.instMonoidSubtypeMem {S : Type u_1} [Semigroup S] {T : Subgroup S} : Monoid ↥T

Equations

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

instance Semigroup.Subgroup.instInvSubtypeMem {S : Type u_1} [Semigroup S] {T : Subgroup S} : Inv ↥T

Equations

• Semigroup.Subgroup.instInvSubtypeMem = { inv := fun (x : ↥T) => ⟨T.inv ↑x, ⋯⟩ }

@[simp]

theorem Semigroup.Subgroup.inv_def {S : Type u_1} [Semigroup S] {T : Subgroup S} (x : ↥T) : x⁻¹ = ⟨T.inv ↑x, ⋯⟩

instance Semigroup.Subgroup.instGroupSubtypeMem {S : Type u_1} [Semigroup S] {T : Subgroup S} : Group ↥T

Equations

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

def Semigroup.Subgroup.isMaximal {S : Type u_1} [Semigroup S] (H : Subgroup S) : Prop

A maximal subgroup is a subgroup that is not properly contained in any other subgroup.

Equations

• H.isMaximal = ∀ (K : Semigroup.Subgroup S), H ≤ K → H = K

theorem Semigroup.Subgroup.mem_def {S : Type u_1} [Semigroup S] {T : Subgroup S} (x : S) : x ∈ T ↔ x ∈ T.carrier

def Semigroup.Subgroup.bijOn_toEquiv {S : Type u_1} [Semigroup S] {H T : Subgroup S} (f : S → S) (hbij : Set.BijOn f H.carrier T.carrier) : Function.Bijective fun (x : ↥H) => ⟨f ↑x, ⋯⟩

Lift a bijection on the carriers of two subgroups to a bijection on their subtypes.

Equations

• ⋯ = ⋯

noncomputable def Semigroup.Subgroup.hom_of_bijOn {S : Type u_1} [Semigroup S] (H T : Subgroup S) (f : S → S) (hbij : Set.BijOn f H.carrier T.carrier) (hmap : ∀ (x y : S), x ∈ H → y ∈ H → f (x * y) = f x * f y) : ↥H ≃* ↥T

Lift a bijection on the carriers of two subgroups that maps multiplication to an isomorphism between the groups.

Equations

• H.hom_of_bijOn T f hbij hmap = { toFun := fun (x : ↥H) => ⟨f ↑x, ⋯⟩, invFun := Function.surjInv ⋯, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }