mathlib3 documentation

group_theory.submonoid.inverses

Submonoid of inverses #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
@[protected, instance]
noncomputable def submonoid.is_unit.submonoid.group {M : Type u_1} [monoid M] :
group ↥(is_unit.submonoid M)
Equations
source
@[protected, instance]
noncomputable def add_submonoid.is_unit.submonoid.add_group {M : Type u_1} [add_monoid M] :
add_group ↥(is_add_unit.add_submonoid M)
Equations
source
@[protected, instance]
noncomputable def submonoid.is_unit.submonoid.comm_group {M : Type u_1} [comm_monoid M] :
comm_group ↥(is_unit.submonoid M)
Equations
source
@[protected, instance]
noncomputable def add_submonoid.is_unit.submonoid.add_comm_group {M : Type u_1} [add_comm_monoid M] :
add_comm_group ↥(is_add_unit.add_submonoid M)
Equations
source
theorem submonoid.is_unit.submonoid.coe_inv {M : Type u_1} [monoid M] (x : ↥(is_unit.submonoid M)) :
↑x⁻¹ = ↑(is_unit.unit _)⁻¹
source
theorem add_submonoid.is_unit.submonoid.coe_neg {M : Type u_1} [add_monoid M] (x : ↥(is_add_unit.add_submonoid M)) :
↑-x = ↑-is_add_unit.add_unit _
source
def add_submonoid.left_neg {M : Type u_1} [add_monoid M] (S : add_submonoid M) :
add_submonoid M

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

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

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

Equations
source
theorem submonoid.left_inv_left_inv_le {M : Type u_1} [monoid M] (S : submonoid M) :
S.left_inv.left_inv ≤ S
source
theorem add_submonoid.left_neg_left_neg_le {M : Type u_1} [add_monoid M] (S : add_submonoid M) :
S.left_neg.left_neg ≤ S
source
theorem submonoid.unit_mem_left_inv {M : Type u_1} [monoid M] (S : submonoid M) (x : Mˣ) (hx : ↑x ∈ S) :
↑x⁻¹ ∈ S.left_inv
source
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) :
↑-x ∈ S.left_neg
source
theorem submonoid.left_inv_left_inv_eq {M : Type u_1} [monoid M] (S : submonoid M) (hS : S ≤ is_unit.submonoid M) :
S.left_inv.left_inv = S
source
theorem add_submonoid.left_neg_left_neg_eq {M : Type u_1} [add_monoid M] (S : add_submonoid M) (hS : S ≤ is_add_unit.add_submonoid M) :
S.left_neg.left_neg = S
source
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
source
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
source
@[simp]
theorem add_submonoid.add_from_left_neg {M : Type u_1} [add_monoid M] (S : add_submonoid M) (x : ↥(S.left_neg)) :
↑x + ↑(S.from_left_neg x) = 0
source
@[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
source
@[simp]
theorem add_submonoid.from_left_neg_zero {M : Type u_1} [add_monoid M] (S : add_submonoid M) :
S.from_left_neg 0 = 0
source
@[simp]
theorem submonoid.from_left_inv_one {M : Type u_1} [monoid M] (S : submonoid M) :
S.from_left_inv 1 = 1
source
@[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
source
@[simp]
theorem add_submonoid.from_left_neg_add {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) (x : ↥(S.left_neg)) :
↑(S.from_left_neg x) + ↑x = 0
source
theorem add_submonoid.left_neg_le_is_add_unit {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :
S.left_neg ≤ is_add_unit.add_submonoid M
source
theorem submonoid.left_inv_le_is_unit {M : Type u_1} [comm_monoid M] (S : submonoid M) :
S.left_inv ≤ is_unit.submonoid M
source
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
source
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
source
@[simp]
theorem add_submonoid.from_comm_left_neg_apply {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) (ᾰ : ↥(S.left_neg)) :
⇑(S.from_comm_left_neg) ᾰ = S.from_left_neg ᾰ
source
noncomputable def add_submonoid.from_comm_left_neg {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :
↥(S.left_neg) →+ ↥S

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

Equations
source
noncomputable def submonoid.from_comm_left_inv {M : Type u_1} [comm_monoid M] (S : submonoid M) :
↥(S.left_inv) →* ↥S

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

Equations
source
@[simp]
theorem submonoid.from_comm_left_inv_apply {M : Type u_1} [comm_monoid M] (S : submonoid M) (ᾰ : ↥(S.left_inv)) :
⇑(S.from_comm_left_inv) ᾰ = S.from_left_inv ᾰ
source
noncomputable def submonoid.left_inv_equiv {M : Type u_1} [comm_monoid M] (S : submonoid M) (hS : S ≤ is_unit.submonoid M) :
↥(S.left_inv) ≃* ↥S

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

Equations
source
@[simp]
theorem add_submonoid.left_neg_equiv_apply {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) (hS : S ≤ is_add_unit.add_submonoid M) (ᾰ : ↥(S.left_neg)) :
⇑(S.left_neg_equiv hS) ᾰ = S.from_comm_left_neg.to_fun ᾰ
source
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) :
↥(S.left_neg) ≃+ ↥S

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

Equations
source
@[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)) :
⇑(S.left_inv_equiv hS) ᾰ = S.from_comm_left_inv.to_fun ᾰ
source
@[simp]
theorem add_submonoid.from_left_neg_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) :
S.from_left_neg (⇑((S.left_neg_equiv hS).symm) x) = x
source
@[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) :
S.from_left_inv (⇑((S.left_inv_equiv hS).symm) x) = x
source
@[simp]
theorem add_submonoid.left_neg_equiv_symm_from_left_neg {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) (hS : S ≤ is_add_unit.add_submonoid M) (x : ↥(S.left_neg)) :
⇑((S.left_neg_equiv hS).symm) (S.from_left_neg x) = x
source
@[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)) :
⇑((S.left_inv_equiv hS).symm) (S.from_left_inv x) = x
source
theorem add_submonoid.left_neg_equiv_add {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) (hS : S ≤ is_add_unit.add_submonoid M) (x : ↥(S.left_neg)) :
↑(⇑(S.left_neg_equiv hS) x) + ↑x = 0
source
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
source
theorem add_submonoid.add_left_neg_equiv {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) (hS : S ≤ is_add_unit.add_submonoid M) (x : ↥(S.left_neg)) :
↑x + ↑(⇑(S.left_neg_equiv hS) x) = 0
source
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
source
@[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
source
@[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
source
@[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
source
@[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
source
theorem submonoid.left_inv_eq_inv {M : Type u_1} [group M] (S : submonoid M) :
S.left_inv = S⁻¹
source
theorem add_submonoid.left_neg_eq_neg {M : Type u_1} [add_group M] (S : add_submonoid M) :
S.left_neg = -S
source
@[simp]
theorem add_submonoid.from_left_neg_eq_neg {M : Type u_1} [add_group M] (S : add_submonoid M) (x : ↥(S.left_neg)) :
↑(S.from_left_neg x) = -↑x
source
@[simp]
theorem submonoid.from_left_inv_eq_inv {M : Type u_1} [group M] (S : submonoid M) (x : ↥(S.left_inv)) :
↑(S.from_left_inv x) = (↑x)⁻¹
source
@[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) :
↑(⇑((S.left_inv_equiv hS).symm) x) = (↑x)⁻¹
source
@[simp]
theorem add_submonoid.left_neg_equiv_symm_eq_neg {M : Type u_1} [add_comm_group M] (S : add_submonoid M) (hS : S ≤ is_add_unit.add_submonoid M) (x : ↥S) :
↑(⇑((S.left_neg_equiv hS).symm) x) = -↑x