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
GroupTheory.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 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.
theorem
AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_10
{M : Type u_1}
[AddMonoid M]
:
∀ (n : ℕ) (a : ↥(IsAddUnit.addSubmonoid M)), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a
theorem
AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_7
{M : Type u_1}
[AddMonoid M]
:
∀ (a b : ↥(IsAddUnit.addSubmonoid M)), a - b = a - b
theorem
AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_6
{M : Type u_1}
[AddMonoid M]
(x : ↥(IsAddUnit.addSubmonoid M))
:
IsAddUnit ↑{ val := (IsAddUnit.addUnit ⋯).neg, neg := ↑(IsAddUnit.addUnit ⋯), val_neg := ⋯, neg_val := ⋯ }
theorem
AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_8
{M : Type u_1}
[AddMonoid M]
:
∀ (a : ↥(IsAddUnit.addSubmonoid M)), zsmulRec 0 a = zsmulRec 0 a
noncomputable instance
AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid
{M : Type u_1}
[AddMonoid M]
:
Equations
- One or more equations did not get rendered due to their size.
theorem
AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_5
{M : Type u_1}
[AddMonoid M]
(x : ↥(IsAddUnit.addSubmonoid M))
:
↑(IsAddUnit.addUnit ⋯) + (IsAddUnit.addUnit ⋯).neg = 0
theorem
AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_4
{M : Type u_1}
[AddMonoid M]
(x : ↥(IsAddUnit.addSubmonoid M))
:
(IsAddUnit.addUnit ⋯).neg + ↑(IsAddUnit.addUnit ⋯) = 0
noncomputable instance
Submonoid.instGroupSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidSubmonoid
{M : Type u_1}
[Monoid M]
:
Group ↥(IsUnit.submonoid M)
Equations
- Submonoid.instGroupSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidSubmonoid = let __src := inferInstanceAs (Monoid ↥(IsUnit.submonoid M)); Group.mk ⋯
theorem
AddSubmonoid.instAddCommGroupSubtypeMemAddSubmonoidToAddZeroClassToAddMonoidInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_1
{M : Type u_1}
[AddCommMonoid M]
(a : ↥(IsAddUnit.addSubmonoid M))
(b : ↥(IsAddUnit.addSubmonoid M))
:
noncomputable instance
AddSubmonoid.instAddCommGroupSubtypeMemAddSubmonoidToAddZeroClassToAddMonoidInstMembershipInstSetLikeAddSubmonoidAddSubmonoid
{M : Type u_1}
[AddCommMonoid M]
:
Equations
- One or more equations did not get rendered due to their size.
noncomputable instance
Submonoid.instCommGroupSubtypeMemSubmonoidToMulOneClassToMonoidInstMembershipInstSetLikeSubmonoidSubmonoid
{M : Type u_1}
[CommMonoid M]
:
Equations
- Submonoid.instCommGroupSubtypeMemSubmonoidToMulOneClassToMonoidInstMembershipInstSetLikeSubmonoidSubmonoid = let __src := inferInstanceAs (Group ↥(IsUnit.submonoid M)); CommGroup.mk ⋯
theorem
AddSubmonoid.IsUnit.Submonoid.coe_neg
{M : Type u_1}
[AddMonoid M]
(x : ↥(IsAddUnit.addSubmonoid M))
:
↑(-x) = ↑(-IsAddUnit.addUnit ⋯)
theorem
Submonoid.IsUnit.Submonoid.coe_inv
{M : Type u_1}
[Monoid M]
(x : ↥(IsUnit.submonoid M))
:
↑x⁻¹ = ↑(IsUnit.unit ⋯)⁻¹
S.leftNeg is the additive submonoid containing all the left additive inverses of S.
Equations
- AddSubmonoid.leftNeg S = { toAddSubsemigroup := { carrier := {x : M | ∃ (y : ↥S), x + ↑y = 0}, add_mem' := ⋯ }, zero_mem' := ⋯ }
Instances For
theorem
AddSubmonoid.addUnit_mem_leftNeg
{M : Type u_1}
[AddMonoid M]
(S : AddSubmonoid M)
(x : AddUnits M)
(hx : ↑x ∈ S)
:
↑(-x) ∈ AddSubmonoid.leftNeg S
theorem
Submonoid.unit_mem_leftInv
{M : Type u_1}
[Monoid M]
(S : Submonoid M)
(x : Mˣ)
(hx : ↑x ∈ S)
:
↑x⁻¹ ∈ Submonoid.leftInv S
theorem
AddSubmonoid.leftNeg_leftNeg_eq
{M : Type u_1}
[AddMonoid M]
(S : AddSubmonoid M)
(hS : S ≤ IsAddUnit.addSubmonoid M)
:
theorem
Submonoid.leftInv_leftInv_eq
{M : Type u_1}
[Monoid M]
(S : Submonoid M)
(hS : S ≤ IsUnit.submonoid M)
:
noncomputable def
AddSubmonoid.fromLeftNeg
{M : Type u_1}
[AddMonoid M]
(S : AddSubmonoid M)
:
↥(AddSubmonoid.leftNeg S) → ↥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
Instances For
theorem
AddSubmonoid.fromLeftNeg.proof_1
{M : Type u_1}
[AddMonoid M]
(S : AddSubmonoid M)
(x : ↥(AddSubmonoid.leftNeg S))
:
↑x ∈ AddSubmonoid.leftNeg S
noncomputable def
Submonoid.fromLeftInv
{M : Type u_1}
[Monoid M]
(S : Submonoid M)
:
↥(Submonoid.leftInv S) → ↥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
Instances For
@[simp]
theorem
AddSubmonoid.add_fromLeftNeg
{M : Type u_1}
[AddMonoid M]
(S : AddSubmonoid M)
(x : ↥(AddSubmonoid.leftNeg S))
:
↑x + ↑(AddSubmonoid.fromLeftNeg S x) = 0
@[simp]
theorem
Submonoid.mul_fromLeftInv
{M : Type u_1}
[Monoid M]
(S : Submonoid M)
(x : ↥(Submonoid.leftInv S))
:
↑x * ↑(Submonoid.fromLeftInv S x) = 1
@[simp]
theorem
AddSubmonoid.fromLeftNeg_zero
{M : Type u_1}
[AddMonoid M]
(S : AddSubmonoid M)
:
AddSubmonoid.fromLeftNeg S 0 = 0
@[simp]
theorem
Submonoid.fromLeftInv_one
{M : Type u_1}
[Monoid M]
(S : Submonoid M)
:
Submonoid.fromLeftInv S 1 = 1
@[simp]
theorem
AddSubmonoid.fromLeftNeg_add
{M : Type u_1}
[AddCommMonoid M]
(S : AddSubmonoid M)
(x : ↥(AddSubmonoid.leftNeg S))
:
↑(AddSubmonoid.fromLeftNeg S x) + ↑x = 0
@[simp]
theorem
Submonoid.fromLeftInv_mul
{M : Type u_1}
[CommMonoid M]
(S : Submonoid M)
(x : ↥(Submonoid.leftInv S))
:
↑(Submonoid.fromLeftInv S x) * ↑x = 1
abbrev
AddSubmonoid.leftNeg_le_isAddUnit.match_1
{M : Type u_1}
[AddCommMonoid M]
(S : AddSubmonoid M)
(x : M)
(motive : x ∈ AddSubmonoid.leftNeg S → Prop)
:
∀ (x_1 : x ∈ AddSubmonoid.leftNeg S), (∀ (y : ↥S) (hx : x + ↑y = 0), motive ⋯) → motive x_1
Equations
- ⋯ = ⋯
Instances For
theorem
AddSubmonoid.fromLeftNeg_eq_iff
{M : Type u_1}
[AddCommMonoid M]
(S : AddSubmonoid M)
(a : ↥(AddSubmonoid.leftNeg S))
(b : M)
:
↑(AddSubmonoid.fromLeftNeg S a) = b ↔ ↑a + b = 0
theorem
Submonoid.fromLeftInv_eq_iff
{M : Type u_1}
[CommMonoid M]
(S : Submonoid M)
(a : ↥(Submonoid.leftInv S))
(b : M)
:
↑(Submonoid.fromLeftInv S a) = b ↔ ↑a * b = 1
theorem
AddSubmonoid.fromCommLeftNeg.proof_1
{M : Type u_1}
[AddCommMonoid M]
(S : AddSubmonoid M)
:
AddSubmonoid.fromLeftNeg S 0 = 0
theorem
AddSubmonoid.fromCommLeftNeg.proof_2
{M : Type u_1}
[AddCommMonoid M]
(S : AddSubmonoid M)
(x : ↥(AddSubmonoid.leftNeg S))
(y : ↥(AddSubmonoid.leftNeg S))
:
{ toFun := AddSubmonoid.fromLeftNeg S, map_zero' := ⋯ }.toFun (x + y) = { toFun := AddSubmonoid.fromLeftNeg S, map_zero' := ⋯ }.toFun x + { toFun := AddSubmonoid.fromLeftNeg S, map_zero' := ⋯ }.toFun y
noncomputable def
AddSubmonoid.fromCommLeftNeg
{M : Type u_1}
[AddCommMonoid M]
(S : AddSubmonoid M)
:
↥(AddSubmonoid.leftNeg S) →+ ↥S
The AddMonoidHom from S.leftNeg to S sending an element to its
right additive inverse in S.
Equations
- AddSubmonoid.fromCommLeftNeg S = { toZeroHom := { toFun := AddSubmonoid.fromLeftNeg S, map_zero' := ⋯ }, map_add' := ⋯ }
Instances For
@[simp]
theorem
AddSubmonoid.fromCommLeftNeg_apply
{M : Type u_1}
[AddCommMonoid M]
(S : AddSubmonoid M)
:
∀ (a : ↥(AddSubmonoid.leftNeg S)), (AddSubmonoid.fromCommLeftNeg S) a = AddSubmonoid.fromLeftNeg S a
@[simp]
theorem
Submonoid.fromCommLeftInv_apply
{M : Type u_1}
[CommMonoid M]
(S : Submonoid M)
:
∀ (a : ↥(Submonoid.leftInv S)), (Submonoid.fromCommLeftInv S) a = Submonoid.fromLeftInv S a
noncomputable def
Submonoid.fromCommLeftInv
{M : Type u_1}
[CommMonoid M]
(S : Submonoid M)
:
↥(Submonoid.leftInv S) →* ↥S
The MonoidHom from S.leftInv to S sending an element to its right inverse in S.
Equations
- Submonoid.fromCommLeftInv S = { toOneHom := { toFun := Submonoid.fromLeftInv S, map_one' := ⋯ }, map_mul' := ⋯ }
Instances For
noncomputable def
AddSubmonoid.leftNegEquiv
{M : Type u_1}
[AddCommMonoid M]
(S : AddSubmonoid M)
(hS : S ≤ IsAddUnit.addSubmonoid M)
:
↥(AddSubmonoid.leftNeg S) ≃+ ↥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_5
{M : Type u_1}
[AddCommMonoid M]
(S : AddSubmonoid M)
(x : ↥(AddSubmonoid.leftNeg S))
(y : ↥(AddSubmonoid.leftNeg S))
:
(AddSubmonoid.fromCommLeftNeg S).toFun (x + y) = (AddSubmonoid.fromCommLeftNeg S).toFun x + (AddSubmonoid.fromCommLeftNeg S).toFun y
theorem
AddSubmonoid.leftNegEquiv.proof_1
{M : Type u_1}
[AddCommMonoid M]
(S : AddSubmonoid M)
(hS : S ≤ IsAddUnit.addSubmonoid M)
(x : ↥S)
:
↑x ∈ IsAddUnit.addSubmonoid M
theorem
AddSubmonoid.leftNegEquiv.proof_2
{M : Type u_1}
[AddCommMonoid M]
(S : AddSubmonoid M)
(hS : S ≤ IsAddUnit.addSubmonoid M)
(x : ↥S)
:
↑(Classical.choose ⋯) = ↑x
theorem
AddSubmonoid.leftNegEquiv.proof_3
{M : Type u_1}
[AddCommMonoid M]
(S : AddSubmonoid M)
(hS : S ≤ IsAddUnit.addSubmonoid M)
(x : ↥(AddSubmonoid.leftNeg S))
:
(fun (x : ↥S) => (fun (x' : AddUnits M) (hx : ↑x' = ↑x) => { val := x'.neg, property := ⋯ }) (Classical.choose ⋯) ⋯)
((AddSubmonoid.fromCommLeftNeg S).toFun x) = x
theorem
AddSubmonoid.leftNegEquiv.proof_4
{M : Type u_1}
[AddCommMonoid M]
(S : AddSubmonoid M)
(hS : S ≤ IsAddUnit.addSubmonoid M)
(x : ↥S)
:
(AddSubmonoid.fromCommLeftNeg S).toFun
((fun (x : ↥S) =>
(fun (x' : AddUnits M) (hx : ↑x' = ↑x) => { val := x'.neg, property := ⋯ }) (Classical.choose ⋯) ⋯)
x) = x
@[simp]
theorem
AddSubmonoid.leftNegEquiv_apply
{M : Type u_1}
[AddCommMonoid M]
(S : AddSubmonoid M)
(hS : S ≤ IsAddUnit.addSubmonoid M)
:
∀ (a : ↥(AddSubmonoid.leftNeg S)), (AddSubmonoid.leftNegEquiv S hS) a = (AddSubmonoid.fromCommLeftNeg S).toFun a
@[simp]
theorem
Submonoid.leftInvEquiv_apply
{M : Type u_1}
[CommMonoid M]
(S : Submonoid M)
(hS : S ≤ IsUnit.submonoid M)
:
∀ (a : ↥(Submonoid.leftInv S)), (Submonoid.leftInvEquiv S hS) a = (Submonoid.fromCommLeftInv S).toFun a
noncomputable def
Submonoid.leftInvEquiv
{M : Type u_1}
[CommMonoid M]
(S : Submonoid M)
(hS : S ≤ IsUnit.submonoid M)
:
↥(Submonoid.leftInv S) ≃* ↥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 : ↥S)
:
AddSubmonoid.fromLeftNeg S ((AddEquiv.symm (AddSubmonoid.leftNegEquiv S hS)) x) = x
@[simp]
theorem
Submonoid.fromLeftInv_leftInvEquiv_symm
{M : Type u_1}
[CommMonoid M]
(S : Submonoid M)
(hS : S ≤ IsUnit.submonoid M)
(x : ↥S)
:
Submonoid.fromLeftInv S ((MulEquiv.symm (Submonoid.leftInvEquiv S hS)) x) = x
@[simp]
theorem
AddSubmonoid.leftNegEquiv_symm_fromLeftNeg
{M : Type u_1}
[AddCommMonoid M]
(S : AddSubmonoid M)
(hS : S ≤ IsAddUnit.addSubmonoid M)
(x : ↥(AddSubmonoid.leftNeg S))
:
(AddEquiv.symm (AddSubmonoid.leftNegEquiv S hS)) (AddSubmonoid.fromLeftNeg S x) = x
@[simp]
theorem
Submonoid.leftInvEquiv_symm_fromLeftInv
{M : Type u_1}
[CommMonoid M]
(S : Submonoid M)
(hS : S ≤ IsUnit.submonoid M)
(x : ↥(Submonoid.leftInv S))
:
(MulEquiv.symm (Submonoid.leftInvEquiv S hS)) (Submonoid.fromLeftInv S x) = x
theorem
AddSubmonoid.leftNegEquiv_add
{M : Type u_1}
[AddCommMonoid M]
(S : AddSubmonoid M)
(hS : S ≤ IsAddUnit.addSubmonoid M)
(x : ↥(AddSubmonoid.leftNeg S))
:
↑((AddSubmonoid.leftNegEquiv S hS) x) + ↑x = 0
theorem
Submonoid.leftInvEquiv_mul
{M : Type u_1}
[CommMonoid M]
(S : Submonoid M)
(hS : S ≤ IsUnit.submonoid M)
(x : ↥(Submonoid.leftInv S))
:
↑((Submonoid.leftInvEquiv S hS) x) * ↑x = 1
theorem
AddSubmonoid.add_leftNegEquiv
{M : Type u_1}
[AddCommMonoid M]
(S : AddSubmonoid M)
(hS : S ≤ IsAddUnit.addSubmonoid M)
(x : ↥(AddSubmonoid.leftNeg S))
:
↑x + ↑((AddSubmonoid.leftNegEquiv S hS) x) = 0
theorem
Submonoid.mul_leftInvEquiv
{M : Type u_1}
[CommMonoid M]
(S : Submonoid M)
(hS : S ≤ IsUnit.submonoid M)
(x : ↥(Submonoid.leftInv S))
:
↑x * ↑((Submonoid.leftInvEquiv S hS) x) = 1
@[simp]
theorem
AddSubmonoid.leftNegEquiv_symm_add
{M : Type u_1}
[AddCommMonoid M]
(S : AddSubmonoid M)
(hS : S ≤ IsAddUnit.addSubmonoid M)
(x : ↥S)
:
↑((AddEquiv.symm (AddSubmonoid.leftNegEquiv S hS)) x) + ↑x = 0
@[simp]
theorem
Submonoid.leftInvEquiv_symm_mul
{M : Type u_1}
[CommMonoid M]
(S : Submonoid M)
(hS : S ≤ IsUnit.submonoid M)
(x : ↥S)
:
↑((MulEquiv.symm (Submonoid.leftInvEquiv S hS)) x) * ↑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 + ↑((AddEquiv.symm (AddSubmonoid.leftNegEquiv S hS)) 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 * ↑((MulEquiv.symm (Submonoid.leftInvEquiv S hS)) x) = 1
theorem
Submonoid.leftInv_eq_inv
{M : Type u_1}
[Group M]
(S : Submonoid M)
:
Submonoid.leftInv S = S⁻¹
@[simp]
theorem
AddSubmonoid.fromLeftNeg_eq_neg
{M : Type u_1}
[AddGroup M]
(S : AddSubmonoid M)
(x : ↥(AddSubmonoid.leftNeg S))
:
↑(AddSubmonoid.fromLeftNeg S x) = -↑x
@[simp]
theorem
Submonoid.fromLeftInv_eq_inv
{M : Type u_1}
[Group M]
(S : Submonoid M)
(x : ↥(Submonoid.leftInv S))
:
↑(Submonoid.fromLeftInv S 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)
:
↑((AddEquiv.symm (AddSubmonoid.leftNegEquiv S hS)) 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)
:
↑((MulEquiv.symm (Submonoid.leftInvEquiv S hS)) x) = (↑x)⁻¹