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.

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 for more details on related constructions.

TODO #

Define the submonoid of right inverses and two-sided inverses. See the comments of #10679 for a possible implementation.

∀ (n : ) (a : ), zsmulRec () a = zsmulRec () a
IsAddUnit { val := .neg, neg := , val_neg := , neg_val := }
∀ (a b : ), a - b = a - b
Equations
∀ (a : ), zsmulRec 0 a = zsmulRec 0 a
∀ (n : ) (a : ), zsmulRec (Int.ofNat n.succ) a = zsmulRec (Int.ofNat n.succ) a
noncomputable instance Submonoid.instGroupSubtypeMemSubmonoid {M : Type u_1} [] :
Equations
• Submonoid.instGroupSubtypeMemSubmonoid = let __src := ;
a + b = b + a
Equations
noncomputable instance Submonoid.instCommGroupSubtypeMemSubmonoid {M : Type u_1} [] :
Equations
• Submonoid.instCommGroupSubtypeMemSubmonoid = let __src := ;
theorem AddSubmonoid.IsUnit.Submonoid.coe_neg {M : Type u_1} [] (x : ) :
(-x) =
theorem Submonoid.IsUnit.Submonoid.coe_inv {M : Type u_1} [] (x : ()) :
x⁻¹ = ()⁻¹
theorem AddSubmonoid.leftNeg.proof_2 {M : Type u_1} [] (S : ) :
∃ (y : S), 0 + y = 0
def AddSubmonoid.leftNeg {M : Type u_1} [] (S : ) :

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 AddSubmonoid.leftNeg.proof_1 {M : Type u_1} [] (S : ) {a : M} (_b : M) :
a {x : M | ∃ (y : S), x + y = 0}_b {x : M | ∃ (y : S), x + y = 0}a + _b {x : M | ∃ (y : S), x + y = 0}
abbrev AddSubmonoid.leftNeg.match_1 {M : Type u_1} [] (S : ) (_b : M) (motive : _b {x : M | ∃ (y : S), x + y = 0}Prop) :
∀ (x : _b {x : M | ∃ (y : S), x + y = 0}), (∀ (b' : S) (hb : _b + b' = 0), motive )motive x
Equations
• =
Instances For
def Submonoid.leftInv {M : Type u_1} [] (S : ) :

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
theorem AddSubmonoid.leftNeg_leftNeg_le {M : Type u_1} [] (S : ) :
S.leftNeg.leftNeg S
theorem Submonoid.leftInv_leftInv_le {M : Type u_1} [] (S : ) :
S.leftInv.leftInv S
theorem AddSubmonoid.addUnit_mem_leftNeg {M : Type u_1} [] (S : ) (x : ) (hx : x S) :
(-x) S.leftNeg
theorem Submonoid.unit_mem_leftInv {M : Type u_1} [] (S : ) (x : Mˣ) (hx : x S) :
x⁻¹ S.leftInv
theorem AddSubmonoid.leftNeg_leftNeg_eq {M : Type u_1} [] (S : ) (hS : ) :
S.leftNeg.leftNeg = S
theorem Submonoid.leftInv_leftInv_eq {M : Type u_1} [] (S : ) (hS : ) :
S.leftInv.leftInv = S
noncomputable def AddSubmonoid.fromLeftNeg {M : Type u_1} [] (S : ) :
S.leftNegS

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 =
Instances For
theorem AddSubmonoid.fromLeftNeg.proof_1 {M : Type u_1} [] (S : ) (x : S.leftNeg) :
x S.leftNeg
noncomputable def Submonoid.fromLeftInv {M : Type u_1} [] (S : ) :
S.leftInvS

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 =
Instances For
@[simp]
theorem AddSubmonoid.add_fromLeftNeg {M : Type u_1} [] (S : ) (x : S.leftNeg) :
x + (S.fromLeftNeg x) = 0
@[simp]
theorem Submonoid.mul_fromLeftInv {M : Type u_1} [] (S : ) (x : S.leftInv) :
x * (S.fromLeftInv x) = 1
@[simp]
theorem AddSubmonoid.fromLeftNeg_zero {M : Type u_1} [] (S : ) :
S.fromLeftNeg 0 = 0
@[simp]
theorem Submonoid.fromLeftInv_one {M : Type u_1} [] (S : ) :
S.fromLeftInv 1 = 1
@[simp]
theorem AddSubmonoid.fromLeftNeg_add {M : Type u_1} [] (S : ) (x : S.leftNeg) :
(S.fromLeftNeg x) + x = 0
@[simp]
theorem Submonoid.fromLeftInv_mul {M : Type u_1} [] (S : ) (x : S.leftInv) :
(S.fromLeftInv x) * x = 1
S.leftNeg
abbrev AddSubmonoid.leftNeg_le_isAddUnit.match_1 {M : Type u_1} [] (S : ) (x : M) (motive : x S.leftNegProp) :
∀ (x_1 : x S.leftNeg), (∀ (y : S) (hx : x + y = 0), motive )motive x_1
Equations
• =
Instances For
theorem Submonoid.leftInv_le_isUnit {M : Type u_1} [] (S : ) :
S.leftInv
theorem AddSubmonoid.fromLeftNeg_eq_iff {M : Type u_1} [] (S : ) (a : S.leftNeg) (b : M) :
(S.fromLeftNeg a) = b a + b = 0
theorem Submonoid.fromLeftInv_eq_iff {M : Type u_1} [] (S : ) (a : S.leftInv) (b : M) :
(S.fromLeftInv a) = b a * b = 1
theorem AddSubmonoid.fromCommLeftNeg.proof_2 {M : Type u_1} [] (S : ) (x : S.leftNeg) (y : S.leftNeg) :
{ toFun := S.fromLeftNeg, map_zero' := }.toFun (x + y) = { toFun := S.fromLeftNeg, map_zero' := }.toFun x + { toFun := S.fromLeftNeg, map_zero' := }.toFun y
noncomputable def AddSubmonoid.fromCommLeftNeg {M : Type u_1} [] (S : ) :
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
theorem AddSubmonoid.fromCommLeftNeg.proof_1 {M : Type u_1} [] (S : ) :
S.fromLeftNeg 0 = 0
@[simp]
theorem Submonoid.fromCommLeftInv_apply {M : Type u_1} [] (S : ) :
∀ (a : S.leftInv), S.fromCommLeftInv a = S.fromLeftInv a
@[simp]
theorem AddSubmonoid.fromCommLeftNeg_apply {M : Type u_1} [] (S : ) :
∀ (a : S.leftNeg), S.fromCommLeftNeg a = S.fromLeftNeg a
noncomputable def Submonoid.fromCommLeftInv {M : Type u_1} [] (S : ) :
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.leftNegEquiv {M : Type u_1} [] (S : ) (hS : ) :
S.leftNeg ≃+ S

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddSubmonoid.leftNegEquiv.proof_1 {M : Type u_1} [] (S : ) (hS : ) (x : S) :
theorem AddSubmonoid.leftNegEquiv.proof_4 {M : Type u_1} [] (S : ) (hS : ) (x : S) :
(S.fromCommLeftNeg).toFun ((fun (x : S) => (fun (x' : ) (hx : x' = x) => x'.neg, ) () ) x) = x
theorem AddSubmonoid.leftNegEquiv.proof_5 {M : Type u_1} [] (S : ) (x : S.leftNeg) (y : S.leftNeg) :
(S.fromCommLeftNeg).toFun (x + y) = (S.fromCommLeftNeg).toFun x + (S.fromCommLeftNeg).toFun y
theorem AddSubmonoid.leftNegEquiv.proof_3 {M : Type u_1} [] (S : ) (hS : ) (x : S.leftNeg) :
(fun (x : S) => (fun (x' : ) (hx : x' = x) => x'.neg, ) () ) ((S.fromCommLeftNeg).toFun x) = x
theorem AddSubmonoid.leftNegEquiv.proof_2 {M : Type u_1} [] (S : ) (hS : ) (x : S) :
() = x
@[simp]
theorem AddSubmonoid.leftNegEquiv_apply {M : Type u_1} [] (S : ) (hS : ) :
∀ (a : S.leftNeg), (S.leftNegEquiv hS) a = (S.fromCommLeftNeg).toFun a
@[simp]
theorem Submonoid.leftInvEquiv_apply {M : Type u_1} [] (S : ) (hS : ) :
∀ (a : S.leftInv), (S.leftInvEquiv hS) a = (S.fromCommLeftInv).toFun a
noncomputable def Submonoid.leftInvEquiv {M : Type u_1} [] (S : ) (hS : ) :
S.leftInv ≃* S

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AddSubmonoid.fromLeftNeg_leftNegEquiv_symm {M : Type u_1} [] (S : ) (hS : ) (x : S) :
S.fromLeftNeg ((S.leftNegEquiv hS).symm x) = x
@[simp]
theorem Submonoid.fromLeftInv_leftInvEquiv_symm {M : Type u_1} [] (S : ) (hS : ) (x : S) :
S.fromLeftInv ((S.leftInvEquiv hS).symm x) = x
@[simp]
theorem AddSubmonoid.leftNegEquiv_symm_fromLeftNeg {M : Type u_1} [] (S : ) (hS : ) (x : S.leftNeg) :
(S.leftNegEquiv hS).symm (S.fromLeftNeg x) = x
@[simp]
theorem Submonoid.leftInvEquiv_symm_fromLeftInv {M : Type u_1} [] (S : ) (hS : ) (x : S.leftInv) :
(S.leftInvEquiv hS).symm (S.fromLeftInv x) = x
theorem AddSubmonoid.leftNegEquiv_add {M : Type u_1} [] (S : ) (hS : ) (x : S.leftNeg) :
((S.leftNegEquiv hS) x) + x = 0
theorem Submonoid.leftInvEquiv_mul {M : Type u_1} [] (S : ) (hS : ) (x : S.leftInv) :
((S.leftInvEquiv hS) x) * x = 1
theorem AddSubmonoid.add_leftNegEquiv {M : Type u_1} [] (S : ) (hS : ) (x : S.leftNeg) :
x + ((S.leftNegEquiv hS) x) = 0
theorem Submonoid.mul_leftInvEquiv {M : Type u_1} [] (S : ) (hS : ) (x : S.leftInv) :
x * ((S.leftInvEquiv hS) x) = 1
@[simp]
theorem AddSubmonoid.leftNegEquiv_symm_add {M : Type u_1} [] (S : ) (hS : ) (x : S) :
((S.leftNegEquiv hS).symm x) + x = 0
@[simp]
theorem Submonoid.leftInvEquiv_symm_mul {M : Type u_1} [] (S : ) (hS : ) (x : S) :
((S.leftInvEquiv hS).symm x) * x = 1
@[simp]
theorem AddSubmonoid.add_leftNegEquiv_symm {M : Type u_1} [] (S : ) (hS : ) (x : S) :
x + ((S.leftNegEquiv hS).symm x) = 0
@[simp]
theorem Submonoid.mul_leftInvEquiv_symm {M : Type u_1} [] (S : ) (hS : ) (x : S) :
x * ((S.leftInvEquiv hS).symm x) = 1
theorem AddSubmonoid.leftNeg_eq_neg {M : Type u_1} [] (S : ) :
S.leftNeg = -S
theorem Submonoid.leftInv_eq_inv {M : Type u_1} [] (S : ) :
S.leftInv = S⁻¹
@[simp]
theorem AddSubmonoid.fromLeftNeg_eq_neg {M : Type u_1} [] (S : ) (x : S.leftNeg) :
(S.fromLeftNeg x) = -x
@[simp]
theorem Submonoid.fromLeftInv_eq_inv {M : Type u_1} [] (S : ) (x : S.leftInv) :
(S.fromLeftInv x) = (x)⁻¹
@[simp]
theorem AddSubmonoid.leftNegEquiv_symm_eq_neg {M : Type u_1} [] (S : ) (hS : ) (x : S) :
((S.leftNegEquiv hS).symm x) = -x
@[simp]
theorem Submonoid.leftInvEquiv_symm_eq_inv {M : Type u_1} [] (S : ) (hS : ) (x : S) :
((S.leftInvEquiv hS).symm x) = (x)⁻¹