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 containing all units that are in N. See the implementation notes of Mathlib/GroupTheory/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.

noncomputable instance Submonoid.instGroupSubtypeMemSubmonoid {M : Type u_1} [Monoid M] :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
def Submonoid.leftInv {M : Type u_1} [Monoid M] (S : 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

    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
      theorem Submonoid.unit_mem_leftInv {M : Type u_1} [Monoid M] (S : Submonoid M) (x : Mˣ) (hx : x S) :
      theorem AddSubmonoid.addUnit_mem_leftNeg {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : AddUnits M) (hx : x S) :
      ↑(-x) S.leftNeg
      noncomputable def Submonoid.fromLeftInv {M : Type u_1} [Monoid M] (S : Submonoid M) :
      S.leftInvS

      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
        noncomputable def AddSubmonoid.fromLeftNeg {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
        S.leftNegS

        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
          @[simp]
          theorem Submonoid.mul_fromLeftInv {M : Type u_1} [Monoid M] (S : Submonoid M) (x : S.leftInv) :
          x * (S.fromLeftInv x) = 1
          @[simp]
          theorem AddSubmonoid.add_fromLeftNeg {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : S.leftNeg) :
          x + (S.fromLeftNeg x) = 0
          @[simp]
          theorem Submonoid.fromLeftInv_one {M : Type u_1} [Monoid M] (S : Submonoid M) :
          @[simp]
          @[simp]
          theorem Submonoid.fromLeftInv_mul {M : Type u_1} [CommMonoid M] (S : Submonoid M) (x : S.leftInv) :
          (S.fromLeftInv x) * x = 1
          @[simp]
          theorem AddSubmonoid.fromLeftNeg_add {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : S.leftNeg) :
          (S.fromLeftNeg x) + x = 0
          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
          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
          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
          Instances For
            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
            Instances For
              @[simp]
              theorem AddSubmonoid.fromCommLeftNeg_apply {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (a✝ : S.leftNeg) :
              @[simp]
              theorem Submonoid.fromCommLeftInv_apply {M : Type u_1} [CommMonoid M] (S : Submonoid M) (a✝ : S.leftInv) :
              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
              Instances For
                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
                Instances For
                  @[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✝
                  @[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✝
                  @[simp]
                  theorem Submonoid.fromLeftInv_leftInvEquiv_symm {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S IsUnit.submonoid M) (x : S) :
                  @[simp]
                  theorem Submonoid.leftInvEquiv_symm_fromLeftInv {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S IsUnit.submonoid M) (x : S.leftInv) :
                  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
                  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
                  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
                  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
                  @[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
                  @[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
                  @[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
                  @[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
                  @[simp]
                  theorem Submonoid.fromLeftInv_eq_inv {M : Type u_1} [Group M] (S : Submonoid M) (x : S.leftInv) :
                  (S.fromLeftInv x) = (↑x)⁻¹
                  @[simp]
                  theorem AddSubmonoid.fromLeftNeg_eq_neg {M : Type u_1} [AddGroup M] (S : AddSubmonoid M) (x : S.leftNeg) :
                  (S.fromLeftNeg 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) :
                  ((S.leftInvEquiv hS).symm 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) :
                  ((S.leftNegEquiv hS).symm x) = -x