Documentation

Mathlib.GroupTheory.Submonoid.Inverses

Submonoid of inverses #

Given a submonoid N of a monoid M, we define the submonoid N.leftInv as the submonoid of left inverses of N. When M is commutative, we may define fromCommLeftInv : N.leftInv →* N since the inverses are unique. When N ≤ IsUnit.Submonoid M, this is precisely the pointwise inverse of N, and we may define leftInvEquiv : S.leftInv ≃* S.

For the pointwise inverse of submonoids of groups, please refer to the file Mathlib/Algebra/Group/Submonoid/Pointwise.lean.

N.leftInv is distinct from N.units, which is the subgroup of Mˣ containing all units that are in N. See the implementation notes of Mathlib/GroupTheory/Submonoid/Units.lean for more details on related constructions.

TODO #

Define the submonoid of right inverses and two-sided inverses. See the comments of https://github.com/leanprover-community/mathlib4/pull/10679 for a possible implementation.

noncomputable instance Submonoid.instGroupSubtypeMemSubmonoid {M : Type u_1} [Monoid M] :

Group ↥(IsUnit.submonoid M)

Equations

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

noncomputable instance AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid {M : Type u_1} [AddMonoid M] :

AddGroup ↥(IsAddUnit.addSubmonoid M)

Equations

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

noncomputable instance Submonoid.instCommGroupSubtypeMemSubmonoid {M : Type u_1} [CommMonoid M] :

CommGroup ↥(IsUnit.submonoid M)

Equations

Submonoid.instCommGroupSubtypeMemSubmonoid = { toGroup := inferInstanceAs (Group ↥(IsUnit.submonoid M)), mul_comm := ⋯ }

noncomputable instance AddSubmonoid.instAddCommGroupSubtypeMemAddSubmonoid {M : Type u_1} [AddCommMonoid M] :

AddCommGroup ↥(IsAddUnit.addSubmonoid M)

Equations

AddSubmonoid.instAddCommGroupSubtypeMemAddSubmonoid = { toAddGroup := inferInstanceAs (AddGroup ↥(IsAddUnit.addSubmonoid M)), add_comm := ⋯ }

theorem Submonoid.IsUnit.Submonoid.coe_inv {M : Type u_1} [Monoid M] (x : ↥(IsUnit.submonoid M)) :

↑x⁻¹ = ↑(IsUnit.unit ⋯)⁻¹

theorem AddSubmonoid.IsUnit.Submonoid.coe_neg {M : Type u_1} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) :

↑(-x) = ↑(-IsAddUnit.addUnit ⋯)

def Submonoid.leftInv {M : Type u_1} [Monoid M] (S : Submonoid M) :

S.leftInv is the submonoid containing all the left inverses of S.

Equations

S.leftInv = { carrier := {x : M | ∃ (y : ↥S), x * ↑y = 1}, mul_mem' := ⋯, one_mem' := ⋯ }

Instances For

def AddSubmonoid.leftNeg {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :

S.leftNeg is the additive submonoid containing all the left additive inverses of S.

Equations

S.leftNeg = { carrier := {x : M | ∃ (y : ↥S), x + ↑y = 0}, add_mem' := ⋯, zero_mem' := ⋯ }

Instances For

theorem Submonoid.leftInv_leftInv_le {M : Type u_1} [Monoid M] (S : Submonoid M) :

S.leftInv.leftInv ≤ S

theorem AddSubmonoid.leftNeg_leftNeg_le {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :

S.leftNeg.leftNeg ≤ S

theorem Submonoid.unit_mem_leftInv {M : Type u_1} [Monoid M] (S : Submonoid M) (x : Mˣ) (hx : ↑x ∈ S) :

↑x⁻¹ ∈ S.leftInv

theorem AddSubmonoid.addUnit_mem_leftNeg {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : AddUnits M) (hx : ↑x ∈ S) :

↑(-x) ∈ S.leftNeg

theorem Submonoid.leftInv_leftInv_eq {M : Type u_1} [Monoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) :

S.leftInv.leftInv = S

theorem AddSubmonoid.leftNeg_leftNeg_eq {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) :

S.leftNeg.leftNeg = S

noncomputable def Submonoid.fromLeftInv {M : Type u_1} [Monoid M] (S : Submonoid M) :

↥S.leftInv → ↥S

The function from S.leftInv to S sending an element to its right inverse in S. This is a MonoidHom when M is commutative.

Equations

S.fromLeftInv x = Exists.choose ⋯

Instances For

noncomputable def AddSubmonoid.fromLeftNeg {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :

↥S.leftNeg → ↥S

The function from S.leftAdd to S sending an element to its right additive inverse in S. This is an AddMonoidHom when M is commutative.

Equations

S.fromLeftNeg x = Exists.choose ⋯

Instances For

@[simp]

theorem Submonoid.mul_fromLeftInv {M : Type u_1} [Monoid M] (S : Submonoid M) (x : ↥S.leftInv) :

↑x * ↑(S.fromLeftInv x) = 1

@[simp]

theorem AddSubmonoid.add_fromLeftNeg {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : ↥S.leftNeg) :

↑x + ↑(S.fromLeftNeg x) = 0

@[simp]

theorem Submonoid.fromLeftInv_one {M : Type u_1} [Monoid M] (S : Submonoid M) :

S.fromLeftInv 1 = 1

@[simp]

theorem AddSubmonoid.fromLeftNeg_zero {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :

S.fromLeftNeg 0 = 0

@[simp]

theorem Submonoid.fromLeftInv_mul {M : Type u_1} [CommMonoid M] (S : Submonoid M) (x : ↥S.leftInv) :

↑(S.fromLeftInv x) * ↑x = 1

@[simp]

theorem AddSubmonoid.fromLeftNeg_add {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : ↥S.leftNeg) :

↑(S.fromLeftNeg x) + ↑x = 0

theorem Submonoid.leftInv_le_isUnit {M : Type u_1} [CommMonoid M] (S : Submonoid M) :

S.leftInv ≤ IsUnit.submonoid M

theorem AddSubmonoid.leftNeg_le_isAddUnit {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) :

S.leftNeg ≤ IsAddUnit.addSubmonoid M

theorem Submonoid.fromLeftInv_eq_iff {M : Type u_1} [CommMonoid M] (S : Submonoid M) (a : ↥S.leftInv) (b : M) :

↑(S.fromLeftInv a) = b ↔ ↑a * b = 1

theorem AddSubmonoid.fromLeftNeg_eq_iff {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (a : ↥S.leftNeg) (b : M) :

↑(S.fromLeftNeg a) = b ↔ ↑a + b = 0

noncomputable def Submonoid.fromCommLeftInv {M : Type u_1} [CommMonoid M] (S : Submonoid M) :

↥S.leftInv →* ↥S

The MonoidHom from S.leftInv to S sending an element to its right inverse in S.

Equations

S.fromCommLeftInv = { toFun := S.fromLeftInv, map_one' := ⋯, map_mul' := ⋯ }

Instances For

noncomputable def AddSubmonoid.fromCommLeftNeg {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) :

↥S.leftNeg →+ ↥S

The AddMonoidHom from S.leftNeg to S sending an element to its right additive inverse in S.

Equations

S.fromCommLeftNeg = { toFun := S.fromLeftNeg, map_zero' := ⋯, map_add' := ⋯ }

Instances For

@[simp]

theorem AddSubmonoid.fromCommLeftNeg_apply {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (a✝ : ↥S.leftNeg) :

S.fromCommLeftNeg a✝ = S.fromLeftNeg a✝

@[simp]

theorem Submonoid.fromCommLeftInv_apply {M : Type u_1} [CommMonoid M] (S : Submonoid M) (a✝ : ↥S.leftInv) :

S.fromCommLeftInv a✝ = S.fromLeftInv a✝

noncomputable def Submonoid.leftInvEquiv {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) :

↥S.leftInv ≃* ↥S

The submonoid of pointwise inverse of S is MulEquiv to S.

Equations

S.leftInvEquiv hS = { toFun := (↑S.fromCommLeftInv).toFun, invFun := fun (x : ↥S) => ⟨↑(IsUnit.unit ⋯)⁻¹, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Instances For

noncomputable def AddSubmonoid.leftNegEquiv {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) :

↥S.leftNeg ≃+ ↥S

The additive submonoid of pointwise additive inverse of S is AddEquiv to S.

Equations

S.leftNegEquiv hS = { toFun := (↑S.fromCommLeftNeg).toFun, invFun := fun (x : ↥S) => ⟨↑(-IsAddUnit.addUnit ⋯), ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

Instances For

@[simp]

theorem AddSubmonoid.leftNegEquiv_apply {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (a✝ : ↥S.leftNeg) :

(S.leftNegEquiv hS) a✝ = (↑S.fromCommLeftNeg).toFun a✝

@[simp]

theorem Submonoid.leftInvEquiv_apply {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (a✝ : ↥S.leftInv) :

(S.leftInvEquiv hS) a✝ = (↑S.fromCommLeftInv).toFun a✝

@[simp]

theorem Submonoid.fromLeftInv_leftInvEquiv_symm {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S) :

S.fromLeftInv ((S.leftInvEquiv hS).symm x) = x

@[simp]

theorem AddSubmonoid.fromLeftNeg_leftNegEquiv_symm {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S) :

S.fromLeftNeg ((S.leftNegEquiv hS).symm x) = x

@[simp]

theorem Submonoid.leftInvEquiv_symm_fromLeftInv {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S.leftInv) :

(S.leftInvEquiv hS).symm (S.fromLeftInv x) = x

@[simp]

theorem AddSubmonoid.leftNegEquiv_symm_fromLeftNeg {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S.leftNeg) :

(S.leftNegEquiv hS).symm (S.fromLeftNeg x) = x

theorem Submonoid.leftInvEquiv_mul {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S.leftInv) :

↑((S.leftInvEquiv hS) x) * ↑x = 1

theorem AddSubmonoid.leftNegEquiv_add {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S.leftNeg) :

↑((S.leftNegEquiv hS) x) + ↑x = 0

theorem Submonoid.mul_leftInvEquiv {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S.leftInv) :

↑x * ↑((S.leftInvEquiv hS) x) = 1

theorem AddSubmonoid.add_leftNegEquiv {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S.leftNeg) :

↑x + ↑((S.leftNegEquiv hS) x) = 0

@[simp]

theorem Submonoid.leftInvEquiv_symm_mul {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S) :

↑((S.leftInvEquiv hS).symm x) * ↑x = 1

@[simp]

theorem AddSubmonoid.leftNegEquiv_symm_add {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S) :

↑((S.leftNegEquiv hS).symm x) + ↑x = 0

@[simp]

theorem Submonoid.mul_leftInvEquiv_symm {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S) :

↑x * ↑((S.leftInvEquiv hS).symm x) = 1

@[simp]

theorem AddSubmonoid.add_leftNegEquiv_symm {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S) :

↑x + ↑((S.leftNegEquiv hS).symm x) = 0

theorem Submonoid.leftInv_eq_inv {M : Type u_1} [Group M] (S : Submonoid M) :

S.leftInv = S⁻¹

theorem AddSubmonoid.leftNeg_eq_neg {M : Type u_1} [AddGroup M] (S : AddSubmonoid M) :

@[simp]

theorem Submonoid.fromLeftInv_eq_inv {M : Type u_1} [Group M] (S : Submonoid M) (x : ↥S.leftInv) :

↑(S.fromLeftInv x) = (↑x)⁻¹

@[simp]

theorem AddSubmonoid.fromLeftNeg_eq_neg {M : Type u_1} [AddGroup M] (S : AddSubmonoid M) (x : ↥S.leftNeg) :

↑(S.fromLeftNeg x) = -↑x

@[simp]

theorem Submonoid.leftInvEquiv_symm_eq_inv {M : Type u_1} [CommGroup M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S) :

↑((S.leftInvEquiv hS).symm x) = (↑x)⁻¹

@[simp]

theorem AddSubmonoid.leftNegEquiv_symm_eq_neg {M : Type u_1} [AddCommGroup M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S) :

↑((S.leftNegEquiv hS).symm x) = -↑x