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.lean.

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/Algebra/Group/Submonoid/Units.lean for more details on related constructions.

TODO #

Define the submonoid of right inverses and two-sided inverses. See the comments of https://github.com/leanprover-community/mathlib4/pull/10679 for a possible implementation.

source
๐Ÿ”ธ coverage
@[implicit_reducible]
noncomputable instance Submonoid.instGroupSubtypeMemSubmonoid {M : Type u_1} [Monoid M] :
Group โ†ฅ(IsUnit.submonoid M)
source
๐Ÿ”ธ coverage
@[implicit_reducible]
noncomputable instance AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid {M : Type u_1} [AddMonoid M] :
AddGroup โ†ฅ(IsAddUnit.addSubmonoid M)
source
๐Ÿ”ธ coverage
@[implicit_reducible]
noncomputable instance Submonoid.instCommGroupSubtypeMemSubmonoid {M : Type u_1} [CommMonoid M] :
CommGroup โ†ฅ(IsUnit.submonoid M)
source
๐Ÿ”ธ coverage
@[implicit_reducible]
noncomputable instance AddSubmonoid.instAddCommGroupSubtypeMemAddSubmonoid {M : Type u_1} [AddCommMonoid M] :
AddCommGroup โ†ฅ(IsAddUnit.addSubmonoid M)
source
๐Ÿ“ coverage
theorem Submonoid.IsUnit.Submonoid.coe_inv {M : Type u_1} [Monoid M] (x : โ†ฅ(IsUnit.submonoid M)) :
โ†‘xโปยน = โ†‘(IsUnit.unit โ‹ฏ)โปยน
source
๐Ÿ“ coverage
theorem AddSubmonoid.IsUnit.Submonoid.coe_neg {M : Type u_1} [AddMonoid M] (x : โ†ฅ(IsAddUnit.addSubmonoid M)) :
โ†‘(-x) = โ†‘(-IsAddUnit.addUnit โ‹ฏ)
source
๐Ÿ”ธ coverage
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.

Instances For
    source
    ๐Ÿ”ธ coverage
    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.

    Instances For
      source
      ๐Ÿ“ coverage
      theorem Submonoid.leftInv_leftInv_le {M : Type u_1} [Monoid M] (S : Submonoid M) :
      S.leftInv.leftInv โ‰ค S
      source
      ๐Ÿ“ coverage
      theorem AddSubmonoid.leftNeg_leftNeg_le {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
      S.leftNeg.leftNeg โ‰ค S
      source
      ๐Ÿ“ coverage
      theorem Submonoid.unit_mem_leftInv {M : Type u_1} [Monoid M] (S : Submonoid M) (x : Mหฃ) (hx : โ†‘x โˆˆ S) :
      โ†‘xโปยน โˆˆ S.leftInv
      source
      ๐Ÿ“ coverage
      theorem AddSubmonoid.addUnit_mem_leftNeg {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : AddUnits M) (hx : โ†‘x โˆˆ S) :
      โ†‘(-x) โˆˆ S.leftNeg
      source
      ๐Ÿ“ coverage
      theorem Submonoid.leftInv_leftInv_eq {M : Type u_1} [Monoid M] (S : Submonoid M) (hS : S โ‰ค IsUnit.submonoid M) :
      S.leftInv.leftInv = S
      source
      ๐Ÿ“ coverage
      theorem AddSubmonoid.leftNeg_leftNeg_eq {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (hS : S โ‰ค IsAddUnit.addSubmonoid M) :
      S.leftNeg.leftNeg = S
      source
      ๐Ÿ”ธ coverage
      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.

      Instances For
        source
        ๐Ÿ”ธ coverage
        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.

        Instances For
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem Submonoid.mul_fromLeftInv {M : Type u_1} [Monoid M] (S : Submonoid M) (x : โ†ฅS.leftInv) :
          โ†‘x * โ†‘(S.fromLeftInv x) = 1
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem AddSubmonoid.add_fromLeftNeg {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : โ†ฅS.leftNeg) :
          โ†‘x + โ†‘(S.fromLeftNeg x) = 0
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem Submonoid.fromLeftInv_one {M : Type u_1} [Monoid M] (S : Submonoid M) :
          S.fromLeftInv 1 = 1
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem AddSubmonoid.fromLeftNeg_zero {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
          S.fromLeftNeg 0 = 0
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem Submonoid.fromLeftInv_mul {M : Type u_1} [CommMonoid M] (S : Submonoid M) (x : โ†ฅS.leftInv) :
          โ†‘(S.fromLeftInv x) * โ†‘x = 1
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem AddSubmonoid.fromLeftNeg_add {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : โ†ฅS.leftNeg) :
          โ†‘(S.fromLeftNeg x) + โ†‘x = 0
          source
          ๐Ÿ“ coverage
          theorem Submonoid.leftInv_le_isUnit {M : Type u_1} [CommMonoid M] (S : Submonoid M) :
          S.leftInv โ‰ค IsUnit.submonoid M
          source
          ๐Ÿ“ coverage
          theorem AddSubmonoid.leftNeg_le_isAddUnit {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) :
          S.leftNeg โ‰ค IsAddUnit.addSubmonoid M
          source
          ๐Ÿ“ coverage
          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
          ๐Ÿ“ coverage
          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
          ๐Ÿ”ธ coverage
          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.

          Instances For
            source
            ๐Ÿ”ธ coverage
            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.

            Instances For
              source
              ๐Ÿ“ coverage
              @[simp]
              theorem Submonoid.fromCommLeftInv_apply {M : Type u_1} [CommMonoid M] (S : Submonoid M) (aโœ : โ†ฅS.leftInv) :
              S.fromCommLeftInv aโœ = S.fromLeftInv aโœ
              source
              ๐Ÿ“ coverage
              @[simp]
              theorem AddSubmonoid.fromCommLeftNeg_apply {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (aโœ : โ†ฅS.leftNeg) :
              S.fromCommLeftNeg aโœ = S.fromLeftNeg aโœ
              source
              ๐Ÿ”ธ coverage
              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.

              Instances For
                source
                ๐Ÿ”ธ coverage
                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.

                Instances For
                  source
                  ๐Ÿ“ coverage
                  @[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
                  ๐Ÿ“ coverage
                  @[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
                  ๐Ÿ“ coverage
                  @[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
                  ๐Ÿ“ coverage
                  @[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
                  ๐Ÿ“ coverage
                  @[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
                  ๐Ÿ“ coverage
                  @[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
                  ๐Ÿ“ coverage
                  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
                  ๐Ÿ“ coverage
                  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
                  ๐Ÿ“ coverage
                  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
                  ๐Ÿ“ coverage
                  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
                  ๐Ÿ“ coverage
                  @[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
                  ๐Ÿ“ coverage
                  @[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
                  ๐Ÿ“ coverage
                  @[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
                  ๐Ÿ“ coverage
                  @[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
                  ๐Ÿ“ coverage
                  theorem Submonoid.leftInv_eq_inv {M : Type u_1} [Group M] (S : Submonoid M) :
                  S.leftInv = Sโปยน
                  source
                  ๐Ÿ“ coverage
                  theorem AddSubmonoid.leftNeg_eq_neg {M : Type u_1} [AddGroup M] (S : AddSubmonoid M) :
                  S.leftNeg = -S
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem Submonoid.fromLeftInv_eq_inv {M : Type u_1} [Group M] (S : Submonoid M) (x : โ†ฅS.leftInv) :
                  โ†‘(S.fromLeftInv x) = (โ†‘x)โปยน
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem AddSubmonoid.fromLeftNeg_eq_neg {M : Type u_1} [AddGroup M] (S : AddSubmonoid M) (x : โ†ฅS.leftNeg) :
                  โ†‘(S.fromLeftNeg x) = -โ†‘x
                  source
                  ๐Ÿ“ coverage
                  @[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)โปยน
                  source
                  ๐Ÿ“ coverage
                  @[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