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.

source
theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_10 {M : Type u_1} [AddMonoid M] :
∀ (n : ℕ) (a : ↥(IsAddUnit.addSubmonoid M)), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a
source
theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_6 {M : Type u_1} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) :
IsAddUnit ↑{ val := (IsAddUnit.addUnit ⋯).neg, neg := ↑(IsAddUnit.addUnit ⋯), val_neg := ⋯, neg_val := ⋯ }
source
theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_7 {M : Type u_1} [AddMonoid M] :
∀ (a b : ↥(IsAddUnit.addSubmonoid M)), a - b = a - b
source
theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_5 {M : Type u_1} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) :
↑(IsAddUnit.addUnit ⋯) + (IsAddUnit.addUnit ⋯).neg = 0
source
noncomputable instance AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid {M : Type u_1} [AddMonoid M] :
AddGroup ↥(IsAddUnit.addSubmonoid M)
Equations
source
theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_4 {M : Type u_1} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) :
(IsAddUnit.addUnit ⋯).neg + ↑(IsAddUnit.addUnit ⋯) = 0
source
theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_1 {M : Type u_1} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) :
↑x ∈ IsAddUnit.addSubmonoid M
source
theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_3 {M : Type u_1} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) :
↑x ∈ IsAddUnit.addSubmonoid M
source
theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_8 {M : Type u_1} [AddMonoid M] :
∀ (a : ↥(IsAddUnit.addSubmonoid M)), zsmulRec 0 a = zsmulRec 0 a
source
theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_11 {M : Type u_1} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) :
-x + x = 0
source
theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_2 {M : Type u_1} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) :
IsAddUnit ↑(-IsAddUnit.addUnit ⋯)
source
theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.proof_9 {M : Type u_1} [AddMonoid M] :
∀ (n : ℕ) (a : ↥(IsAddUnit.addSubmonoid M)), zsmulRec (Int.ofNat n.succ) a = zsmulRec (Int.ofNat n.succ) a
source
noncomputable instance Submonoid.instGroupSubtypeMemSubmonoid {M : Type u_1} [Monoid M] :
Group ↥(IsUnit.submonoid M)
Equations
source
theorem AddSubmonoid.instAddCommGroupSubtypeMemAddSubmonoid.proof_1 {M : Type u_1} [AddCommMonoid M] (a : ↥(IsAddUnit.addSubmonoid M)) (b : ↥(IsAddUnit.addSubmonoid M)) :
a + b = b + a
source
noncomputable instance AddSubmonoid.instAddCommGroupSubtypeMemAddSubmonoid {M : Type u_1} [AddCommMonoid M] :
AddCommGroup ↥(IsAddUnit.addSubmonoid M)
Equations
source
noncomputable instance Submonoid.instCommGroupSubtypeMemSubmonoid {M : Type u_1} [CommMonoid M] :
CommGroup ↥(IsUnit.submonoid M)
Equations
source
theorem AddSubmonoid.IsUnit.Submonoid.coe_neg {M : Type u_1} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) :
↑(-x) = ↑(-IsAddUnit.addUnit ⋯)
source
theorem Submonoid.IsUnit.Submonoid.coe_inv {M : Type u_1} [Monoid M] (x : ↥(IsUnit.submonoid M)) :
↑x⁻¹ = ↑(IsUnit.unit ⋯)⁻¹
source
theorem AddSubmonoid.leftNeg.proof_2 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
∃ (y : ↥S), 0 + ↑y = 0
source
def AddSubmonoid.leftNeg {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
AddSubmonoid M

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
    source
    theorem AddSubmonoid.leftNeg.proof_1 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {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}
    source
    abbrev AddSubmonoid.leftNeg.match_1 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (_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
      source
      def Submonoid.leftInv {M : Type u_1} [Monoid M] (S : Submonoid M) :
      Submonoid M

      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
        source
        theorem AddSubmonoid.leftNeg_leftNeg_le {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
        S.leftNeg.leftNeg ≤ S
        source
        theorem Submonoid.leftInv_leftInv_le {M : Type u_1} [Monoid M] (S : Submonoid M) :
        S.leftInv.leftInv ≤ S
        source
        theorem AddSubmonoid.addUnit_mem_leftNeg {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : AddUnits M) (hx : ↑x ∈ S) :
        ↑(-x) ∈ S.leftNeg
        source
        theorem Submonoid.unit_mem_leftInv {M : Type u_1} [Monoid M] (S : Submonoid M) (x : Mˣ) (hx : ↑x ∈ S) :
        ↑x⁻¹ ∈ S.leftInv
        source
        theorem AddSubmonoid.leftNeg_leftNeg_eq {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) :
        S.leftNeg.leftNeg = S
        source
        theorem Submonoid.leftInv_leftInv_eq {M : Type u_1} [Monoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) :
        S.leftInv.leftInv = S
        source
        noncomputable def AddSubmonoid.fromLeftNeg {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
        ↥S.leftNeg → ↥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
          source
          theorem AddSubmonoid.fromLeftNeg.proof_1 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : ↥S.leftNeg) :
          ↑x ∈ S.leftNeg
          source
          noncomputable def Submonoid.fromLeftInv {M : Type u_1} [Monoid M] (S : Submonoid M) :
          ↥S.leftInv → ↥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
            source
            @[simp]
            theorem AddSubmonoid.add_fromLeftNeg {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : ↥S.leftNeg) :
            ↑x + ↑(S.fromLeftNeg x) = 0
            source
            @[simp]
            theorem Submonoid.mul_fromLeftInv {M : Type u_1} [Monoid M] (S : Submonoid M) (x : ↥S.leftInv) :
            ↑x * ↑(S.fromLeftInv x) = 1
            source
            @[simp]
            theorem AddSubmonoid.fromLeftNeg_zero {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
            S.fromLeftNeg 0 = 0
            source
            @[simp]
            theorem Submonoid.fromLeftInv_one {M : Type u_1} [Monoid M] (S : Submonoid M) :
            S.fromLeftInv 1 = 1
            source
            @[simp]
            theorem AddSubmonoid.fromLeftNeg_add {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : ↥S.leftNeg) :
            ↑(S.fromLeftNeg x) + ↑x = 0
            source
            @[simp]
            theorem Submonoid.fromLeftInv_mul {M : Type u_1} [CommMonoid M] (S : Submonoid M) (x : ↥S.leftInv) :
            ↑(S.fromLeftInv x) * ↑x = 1
            source
            theorem AddSubmonoid.leftNeg_le_isAddUnit {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) :
            S.leftNeg ≤ IsAddUnit.addSubmonoid M
            source
            abbrev AddSubmonoid.leftNeg_le_isAddUnit.match_1 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : M) (motive : x ∈ S.leftNeg → Prop) :
            ∀ (x_1 : x ∈ S.leftNeg), (∀ (y : ↥S) (hx : x + ↑y = 0), motive ⋯) → motive x_1
            Equations
            • ⋯ = ⋯
            Instances For
              source
              theorem Submonoid.leftInv_le_isUnit {M : Type u_1} [CommMonoid M] (S : Submonoid M) :
              S.leftInv ≤ IsUnit.submonoid M
              source
              theorem AddSubmonoid.fromLeftNeg_eq_iff {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (a : ↥S.leftNeg) (b : M) :
              ↑(S.fromLeftNeg a) = b ↔ ↑a + b = 0
              source
              theorem Submonoid.fromLeftInv_eq_iff {M : Type u_1} [CommMonoid M] (S : Submonoid M) (a : ↥S.leftInv) (b : M) :
              ↑(S.fromLeftInv a) = b ↔ ↑a * b = 1
              source
              theorem AddSubmonoid.fromCommLeftNeg.proof_2 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (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
              source
              noncomputable def AddSubmonoid.fromCommLeftNeg {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) :
              ↥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
                source
                theorem AddSubmonoid.fromCommLeftNeg.proof_1 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) :
                S.fromLeftNeg 0 = 0
                source
                @[simp]
                theorem Submonoid.fromCommLeftInv_apply {M : Type u_1} [CommMonoid M] (S : Submonoid M) :
                ∀ (a : ↥S.leftInv), S.fromCommLeftInv a = S.fromLeftInv a
                source
                @[simp]
                theorem AddSubmonoid.fromCommLeftNeg_apply {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) :
                ∀ (a : ↥S.leftNeg), S.fromCommLeftNeg a = S.fromLeftNeg a
                source
                noncomputable def Submonoid.fromCommLeftInv {M : Type u_1} [CommMonoid M] (S : Submonoid M) :
                ↥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
                  source
                  noncomputable def AddSubmonoid.leftNegEquiv {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) :
                  ↥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
                    source
                    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
                    source
                    theorem AddSubmonoid.leftNegEquiv.proof_4 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S) :
                    (↑S.fromCommLeftNeg).toFun ((fun (x : ↥S) => (fun (x' : AddUnits M) (hx : ↑x' = ↑x) => ⟨x'.neg, ⋯⟩) (Classical.choose ⋯) ⋯) x) = x
                    source
                    theorem AddSubmonoid.leftNegEquiv.proof_5 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : ↥S.leftNeg) (y : ↥S.leftNeg) :
                    (↑S.fromCommLeftNeg).toFun (x + y) = (↑S.fromCommLeftNeg).toFun x + (↑S.fromCommLeftNeg).toFun y
                    source
                    theorem AddSubmonoid.leftNegEquiv.proof_3 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S.leftNeg) :
                    (fun (x : ↥S) => (fun (x' : AddUnits M) (hx : ↑x' = ↑x) => ⟨x'.neg, ⋯⟩) (Classical.choose ⋯) ⋯) ((↑S.fromCommLeftNeg).toFun x) = x
                    source
                    theorem AddSubmonoid.leftNegEquiv.proof_2 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S) :
                    ↑(Classical.choose ⋯) = ↑x
                    source
                    @[simp]
                    theorem AddSubmonoid.leftNegEquiv_apply {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) :
                    ∀ (a : ↥S.leftNeg), (S.leftNegEquiv hS) a = (↑S.fromCommLeftNeg).toFun a
                    source
                    @[simp]
                    theorem Submonoid.leftInvEquiv_apply {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) :
                    ∀ (a : ↥S.leftInv), (S.leftInvEquiv hS) a = (↑S.fromCommLeftInv).toFun a
                    source
                    noncomputable def Submonoid.leftInvEquiv {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) :
                    ↥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
                      source
                      @[simp]
                      theorem AddSubmonoid.fromLeftNeg_leftNegEquiv_symm {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S) :
                      S.fromLeftNeg ((S.leftNegEquiv hS).symm x) = x
                      source
                      @[simp]
                      theorem Submonoid.fromLeftInv_leftInvEquiv_symm {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S) :
                      S.fromLeftInv ((S.leftInvEquiv hS).symm x) = x
                      source
                      @[simp]
                      theorem AddSubmonoid.leftNegEquiv_symm_fromLeftNeg {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S.leftNeg) :
                      (S.leftNegEquiv hS).symm (S.fromLeftNeg x) = x
                      source
                      @[simp]
                      theorem Submonoid.leftInvEquiv_symm_fromLeftInv {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S.leftInv) :
                      (S.leftInvEquiv hS).symm (S.fromLeftInv x) = x
                      source
                      theorem AddSubmonoid.leftNegEquiv_add {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S.leftNeg) :
                      ↑((S.leftNegEquiv hS) x) + ↑x = 0
                      source
                      theorem Submonoid.leftInvEquiv_mul {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S.leftInv) :
                      ↑((S.leftInvEquiv hS) x) * ↑x = 1
                      source
                      theorem AddSubmonoid.add_leftNegEquiv {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S.leftNeg) :
                      ↑x + ↑((S.leftNegEquiv hS) x) = 0
                      source
                      theorem Submonoid.mul_leftInvEquiv {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S.leftInv) :
                      ↑x * ↑((S.leftInvEquiv hS) x) = 1
                      source
                      @[simp]
                      theorem AddSubmonoid.leftNegEquiv_symm_add {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S) :
                      ↑((S.leftNegEquiv hS).symm x) + ↑x = 0
                      source
                      @[simp]
                      theorem Submonoid.leftInvEquiv_symm_mul {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S) :
                      ↑((S.leftInvEquiv hS).symm x) * ↑x = 1
                      source
                      @[simp]
                      theorem AddSubmonoid.add_leftNegEquiv_symm {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S) :
                      ↑x + ↑((S.leftNegEquiv hS).symm x) = 0
                      source
                      @[simp]
                      theorem Submonoid.mul_leftInvEquiv_symm {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S) :
                      ↑x * ↑((S.leftInvEquiv hS).symm x) = 1
                      source
                      theorem AddSubmonoid.leftNeg_eq_neg {M : Type u_1} [AddGroup M] (S : AddSubmonoid M) :
                      S.leftNeg = -S
                      source
                      theorem Submonoid.leftInv_eq_inv {M : Type u_1} [Group M] (S : Submonoid M) :
                      S.leftInv = S⁻¹
                      source
                      @[simp]
                      theorem AddSubmonoid.fromLeftNeg_eq_neg {M : Type u_1} [AddGroup M] (S : AddSubmonoid M) (x : ↥S.leftNeg) :
                      ↑(S.fromLeftNeg x) = -↑x
                      source
                      @[simp]
                      theorem Submonoid.fromLeftInv_eq_inv {M : Type u_1} [Group M] (S : Submonoid M) (x : ↥S.leftInv) :
                      ↑(S.fromLeftInv x) = (↑x)⁻¹
                      source
                      @[simp]
                      theorem AddSubmonoid.leftNegEquiv_symm_eq_neg {M : Type u_1} [AddCommGroup M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S) :
                      ↑((S.leftNegEquiv hS).symm x) = -↑x
                      source
                      @[simp]
                      theorem Submonoid.leftInvEquiv_symm_eq_inv {M : Type u_1} [CommGroup M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S) :
                      ↑((S.leftInvEquiv hS).symm x) = (↑x)⁻¹