mathlib documentation

group_theory.submonoid.inverses

Submonoid of inverses #

Given a submonoid N of a monoid M, we define the submonoid N.left_inv as the submonoid of left inverses of N. When M is commutative, we may define from_comm_left_inv : N.left_inv →* N since the inverses are unique. When N ≤ is_unit.submonoid M, this is precisely the pointwise inverse of N, and we may define left_inv_equiv : S.left_inv ≃* S.

For the pointwise inverse of submonoids of groups, please refer to group_theory.submonoid.pointwise.

TODO #

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

@[protected, instance]
noncomputable def submonoid.is_unit.submonoid.group {M : Type u_1} [monoid M] :
Equations
@[protected, instance]
Equations
def add_submonoid.left_neg {M : Type u_1} [add_monoid M] (S : add_submonoid M) :

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

Equations
def submonoid.left_inv {M : Type u_1} [monoid M] (S : submonoid M) :

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

Equations
theorem submonoid.left_inv_left_inv_le {M : Type u_1} [monoid M] (S : submonoid M) :
theorem submonoid.unit_mem_left_inv {M : Type u_1} [monoid M] (S : submonoid M) (x : Mˣ) (hx : x S) :
theorem add_submonoid.add_unit_mem_left_neg {M : Type u_1} [add_monoid M] (S : add_submonoid M) (x : add_units M) (hx : x S) :
theorem submonoid.left_inv_left_inv_eq {M : Type u_1} [monoid M] (S : submonoid M) (hS : S is_unit.submonoid M) :
noncomputable def add_submonoid.from_left_neg {M : Type u_1} [add_monoid M] (S : add_submonoid M) :
(S.left_neg) → S

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

Equations
noncomputable def submonoid.from_left_inv {M : Type u_1} [monoid M] (S : submonoid M) :
(S.left_inv) → S

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

Equations
@[simp]
theorem add_submonoid.add_from_left_neg {M : Type u_1} [add_monoid M] (S : add_submonoid M) (x : (S.left_neg)) :
@[simp]
theorem submonoid.mul_from_left_inv {M : Type u_1} [monoid M] (S : submonoid M) (x : (S.left_inv)) :
(x) * (S.from_left_inv x) = 1
@[simp]
theorem add_submonoid.from_left_neg_zero {M : Type u_1} [add_monoid M] (S : add_submonoid M) :
@[simp]
theorem submonoid.from_left_inv_one {M : Type u_1} [monoid M] (S : submonoid M) :
@[simp]
theorem submonoid.from_left_inv_mul {M : Type u_1} [comm_monoid M] (S : submonoid M) (x : (S.left_inv)) :
((S.from_left_inv x)) * x = 1
@[simp]
theorem add_submonoid.from_left_neg_add {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) (x : (S.left_neg)) :
theorem add_submonoid.from_left_neg_eq_iff {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) (a : (S.left_neg)) (b : M) :
(S.from_left_neg a) = b a + b = 0
theorem submonoid.from_left_inv_eq_iff {M : Type u_1} [comm_monoid M] (S : submonoid M) (a : (S.left_inv)) (b : M) :
(S.from_left_inv a) = b (a) * b = 1
@[simp]
noncomputable def add_submonoid.from_comm_left_neg {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :

The add_monoid_hom from S.left_neg to S sending an element to its right additive inverse in S.

Equations
noncomputable def submonoid.from_comm_left_inv {M : Type u_1} [comm_monoid M] (S : submonoid M) :

The monoid_hom from S.left_inv to S sending an element to its right inverse in S.

Equations
@[simp]
theorem submonoid.from_comm_left_inv_apply {M : Type u_1} [comm_monoid M] (S : submonoid M) (ᾰ : (S.left_inv)) :
noncomputable def submonoid.left_inv_equiv {M : Type u_1} [comm_monoid M] (S : submonoid M) (hS : S is_unit.submonoid M) :

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

Equations
noncomputable def add_submonoid.left_neg_equiv {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) (hS : S is_add_unit.add_submonoid M) :

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

Equations
@[simp]
theorem submonoid.left_inv_equiv_apply {M : Type u_1} [comm_monoid M] (S : submonoid M) (hS : S is_unit.submonoid M) (ᾰ : (S.left_inv)) :
@[simp]
theorem submonoid.from_left_inv_left_inv_equiv_symm {M : Type u_1} [comm_monoid M] (S : submonoid M) (hS : S is_unit.submonoid M) (x : S) :
@[simp]
theorem submonoid.left_inv_equiv_symm_from_left_inv {M : Type u_1} [comm_monoid M] (S : submonoid M) (hS : S is_unit.submonoid M) (x : (S.left_inv)) :
theorem submonoid.left_inv_equiv_mul {M : Type u_1} [comm_monoid M] (S : submonoid M) (hS : S is_unit.submonoid M) (x : (S.left_inv)) :
(((S.left_inv_equiv hS) x)) * x = 1
theorem submonoid.mul_left_inv_equiv {M : Type u_1} [comm_monoid M] (S : submonoid M) (hS : S is_unit.submonoid M) (x : (S.left_inv)) :
(x) * ((S.left_inv_equiv hS) x) = 1
@[simp]
theorem submonoid.left_inv_equiv_symm_mul {M : Type u_1} [comm_monoid M] (S : submonoid M) (hS : S is_unit.submonoid M) (x : S) :
((((S.left_inv_equiv hS).symm) x)) * x = 1
@[simp]
theorem add_submonoid.left_neg_equiv_symm_add {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) (hS : S is_add_unit.add_submonoid M) (x : S) :
(((S.left_neg_equiv hS).symm) x) + x = 0
@[simp]
theorem add_submonoid.add_left_neg_equiv_symm {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) (hS : S is_add_unit.add_submonoid M) (x : S) :
x + (((S.left_neg_equiv hS).symm) x) = 0
@[simp]
theorem submonoid.mul_left_inv_equiv_symm {M : Type u_1} [comm_monoid M] (S : submonoid M) (hS : S is_unit.submonoid M) (x : S) :
(x) * (((S.left_inv_equiv hS).symm) x) = 1
theorem submonoid.left_inv_eq_inv {M : Type u_1} [group M] (S : submonoid M) :
theorem add_submonoid.left_neg_eq_neg {M : Type u_1} [add_group M] (S : add_submonoid M) :
@[simp]
theorem add_submonoid.from_left_neg_eq_neg {M : Type u_1} [add_group M] (S : add_submonoid M) (x : (S.left_neg)) :
@[simp]
theorem submonoid.from_left_inv_eq_inv {M : Type u_1} [group M] (S : submonoid M) (x : (S.left_inv)) :
@[simp]
theorem submonoid.left_inv_equiv_symm_eq_inv {M : Type u_1} [comm_group M] (S : submonoid M) (hS : S is_unit.submonoid M) (x : S) :
@[simp]