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.

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.

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

AddGroup { x : M // x ∈ IsAddUnit.addSubmonoid M }

Equations

AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid = AddGroup.mk ⋯

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_5 {M : Type u_1} [AddMonoid M] (x : { x : M // x ∈ IsAddUnit.addSubmonoid M }) :

↑(IsAddUnit.addUnit ⋯) + (IsAddUnit.addUnit ⋯).neg = 0

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_6 {M : Type u_1} [AddMonoid M] (x : { x : M // x ∈ IsAddUnit.addSubmonoid M }) :

IsAddUnit ↑{ val := (IsAddUnit.addUnit ⋯).neg, neg := ↑(IsAddUnit.addUnit ⋯), val_neg := ⋯, neg_val := ⋯ }

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_7 {M : Type u_1} [AddMonoid M] :

∀ (a b : { x : M // x ∈ IsAddUnit.addSubmonoid M }), a - b = a - b

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_1 {M : Type u_1} [AddMonoid M] (x : { x : M // x ∈ IsAddUnit.addSubmonoid M }) :

↑x ∈ IsAddUnit.addSubmonoid M

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_8 {M : Type u_1} [AddMonoid M] :

∀ (a : { x : M // x ∈ IsAddUnit.addSubmonoid M }), zsmulRec 0 a = zsmulRec 0 a

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_11 {M : Type u_1} [AddMonoid M] (x : { x : M // x ∈ IsAddUnit.addSubmonoid M }) :

-x + x = 0

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_2 {M : Type u_1} [AddMonoid M] (x : { x : M // x ∈ IsAddUnit.addSubmonoid M }) :

IsAddUnit ↑(-IsAddUnit.addUnit ⋯)

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_3 {M : Type u_1} [AddMonoid M] (x : { x : M // x ∈ IsAddUnit.addSubmonoid M }) :

↑x ∈ IsAddUnit.addSubmonoid M

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_4 {M : Type u_1} [AddMonoid M] (x : { x : M // x ∈ IsAddUnit.addSubmonoid M }) :

(IsAddUnit.addUnit ⋯).neg + ↑(IsAddUnit.addUnit ⋯) = 0

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_9 {M : Type u_1} [AddMonoid M] :

∀ (n : ℕ) (a : { x : M // x ∈ IsAddUnit.addSubmonoid M }), zsmulRec (Int.ofNat n.succ) a = zsmulRec (Int.ofNat n.succ) a

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_10 {M : Type u_1} [AddMonoid M] :

∀ (n : ℕ) (a : { x : M // x ∈ IsAddUnit.addSubmonoid M }), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a

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

Group { x : M // x ∈ IsUnit.submonoid M }

Equations

Submonoid.instGroupSubtypeMemSubmonoid = Group.mk ⋯

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

AddCommGroup { x : M // x ∈ IsAddUnit.addSubmonoid M }

Equations

AddSubmonoid.instAddCommGroupSubtypeMemAddSubmonoid = AddCommGroup.mk ⋯

theorem AddSubmonoid.instAddCommGroupSubtypeMemAddSubmonoid.proof_1 {M : Type u_1} [AddCommMonoid M] (a : { x : M // x ∈ IsAddUnit.addSubmonoid M }) (b : { x : M // x ∈ IsAddUnit.addSubmonoid M }) :

a + b = b + a

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

CommGroup { x : M // x ∈ IsUnit.submonoid M }

Equations

Submonoid.instCommGroupSubtypeMemSubmonoid = CommGroup.mk ⋯

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

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

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

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

theorem AddSubmonoid.leftNeg.proof_1 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {a : M} (_b : M) :

a ∈ {x : M | ∃ (y : { x : M // x ∈ S }), x + ↑y = 0} → _b ∈ {x : M | ∃ (y : { x : M // x ∈ S }), x + ↑y = 0} → a + _b ∈ {x : M | ∃ (y : { x : M // x ∈ S }), x + ↑y = 0}

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 : { x : M // x ∈ S }), x + ↑y = 0}, add_mem' := ⋯, zero_mem' := ⋯ }

Instances For

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

∃ (y : { x : M // x ∈ S }), 0 + ↑y = 0

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 : { x : M // x ∈ S }), x * ↑y = 1}, mul_mem' := ⋯, one_mem' := ⋯ }

Instances For

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

S.leftNeg.leftNeg ≤ S

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

S.leftInv.leftInv ≤ S

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.unit_mem_leftInv {M : Type u_1} [Monoid M] (S : Submonoid M) (x : Mˣ) (hx : ↑x ∈ S) :

↑x⁻¹ ∈ S.leftInv

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

S.leftNeg.leftNeg = S

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.fromLeftNeg.proof_1 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : { x : M // x ∈ S.leftNeg }) :

↑x ∈ S.leftNeg

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

{ x : M // x ∈ S.leftNeg } → { x : M // x ∈ 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

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

{ x : M // x ∈ S.leftInv } → { x : M // x ∈ 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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

S.fromLeftNeg 0 = 0

@[simp]

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

S.fromLeftInv 1 = 1

@[simp]

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

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

@[simp]

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

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

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

S.leftNeg ≤ IsAddUnit.addSubmonoid M

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

S.leftInv ≤ IsUnit.submonoid M

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

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

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

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

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

{ x : M // x ∈ S.leftNeg } →+ { x : M // x ∈ 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} [AddCommMonoid M] (S : AddSubmonoid M) :

S.fromLeftNeg 0 = 0

theorem AddSubmonoid.fromCommLeftNeg.proof_2 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : { x : M // x ∈ S.leftNeg }) (y : { x : M // x ∈ S.leftNeg }) :

{ toFun := S.fromLeftNeg, map_zero' := ⋯ }.toFun (x + y) = { toFun := S.fromLeftNeg, map_zero' := ⋯ }.toFun x + { toFun := S.fromLeftNeg, map_zero' := ⋯ }.toFun y

@[simp]

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

∀ (a : { x : M // x ∈ S.leftNeg }), S.fromCommLeftNeg a = S.fromLeftNeg a

@[simp]

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

∀ (a : { x : M // x ∈ S.leftInv }), S.fromCommLeftInv a = S.fromLeftInv a

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

{ x : M // x ∈ S.leftInv } →* { x : M // x ∈ 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

theorem AddSubmonoid.leftNegEquiv.proof_5 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : { x : M // x ∈ S.leftNeg }) (y : { x : M // x ∈ S.leftNeg }) :

(↑S.fromCommLeftNeg).toFun (x + y) = (↑S.fromCommLeftNeg).toFun x + (↑S.fromCommLeftNeg).toFun y

theorem AddSubmonoid.leftNegEquiv.proof_1 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : { x : M // x ∈ S }) :

↑x ∈ IsAddUnit.addSubmonoid M

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

{ x : M // x ∈ S.leftNeg } ≃+ { x : M // x ∈ 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_4 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : { x : M // x ∈ S }) :

(↑S.fromCommLeftNeg).toFun ((fun (x : { x : M // x ∈ S }) => (fun (x' : AddUnits M) (hx : ↑x' = ↑x) => ⟨x'.neg, ⋯⟩) (Classical.choose ⋯) ⋯) x) = x

theorem AddSubmonoid.leftNegEquiv.proof_3 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : { x : M // x ∈ S.leftNeg }) :

(fun (x : { x : M // x ∈ S }) => (fun (x' : AddUnits M) (hx : ↑x' = ↑x) => ⟨x'.neg, ⋯⟩) (Classical.choose ⋯) ⋯) ((↑S.fromCommLeftNeg).toFun x) = x

theorem AddSubmonoid.leftNegEquiv.proof_2 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : { x : M // x ∈ S }) :

↑(Classical.choose ⋯) = ↑x

@[simp]

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

∀ (a : { x : M // x ∈ 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 : { x : M // x ∈ S.leftInv }), (S.leftInvEquiv hS) a = (↑S.fromCommLeftInv).toFun a

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

{ x : M // x ∈ S.leftInv } ≃* { x : M // x ∈ 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} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : { x : M // x ∈ S }) :

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

S.leftNeg = -S

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

S.leftInv = S⁻¹

@[simp]

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

↑(S.fromLeftNeg x) = -↑x

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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