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

Equations
  • AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid = AddGroup.mk
noncomputable instance Submonoid.instGroupSubtypeMemSubmonoid {M : Type u_1} [Monoid M] :
Equations
  • Submonoid.instGroupSubtypeMemSubmonoid = Group.mk
Equations
Equations

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
    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
      theorem AddSubmonoid.leftNeg_leftNeg_le {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
      S.leftNeg.leftNeg S
      theorem Submonoid.leftInv_leftInv_le {M : Type u_1} [Monoid M] (S : Submonoid M) :
      S.leftInv.leftInv S
      theorem AddSubmonoid.addUnit_mem_leftNeg {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : AddUnits M) (hx : x S) :
      (-x) S.leftNeg
      theorem Submonoid.unit_mem_leftInv {M : Type u_1} [Monoid M] (S : Submonoid M) (x : Mˣ) (hx : x S) :
      x⁻¹ S.leftInv
      theorem AddSubmonoid.leftNeg_leftNeg_eq {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (hS : S IsAddUnit.addSubmonoid M) :
      S.leftNeg.leftNeg = S
      theorem Submonoid.leftInv_leftInv_eq {M : Type u_1} [Monoid M] (S : Submonoid M) (hS : S IsUnit.submonoid M) :
      S.leftInv.leftInv = S
      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
        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
          @[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.mul_fromLeftInv {M : Type u_1} [Monoid M] (S : Submonoid M) (x : S.leftInv) :
          x * (S.fromLeftInv x) = 1
          @[simp]
          theorem AddSubmonoid.fromLeftNeg_zero {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
          S.fromLeftNeg 0 = 0
          @[simp]
          theorem Submonoid.fromLeftInv_one {M : Type u_1} [Monoid M] (S : Submonoid M) :
          S.fromLeftInv 1 = 1
          @[simp]
          theorem AddSubmonoid.fromLeftNeg_add {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : S.leftNeg) :
          (S.fromLeftNeg x) + x = 0
          @[simp]
          theorem Submonoid.fromLeftInv_mul {M : Type u_1} [CommMonoid M] (S : Submonoid M) (x : S.leftInv) :
          (S.fromLeftInv x) * x = 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
          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
          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
            @[simp]
            theorem AddSubmonoid.fromCommLeftNeg_apply {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) :
            ∀ (a : S.leftNeg), S.fromCommLeftNeg a = S.fromLeftNeg a
            @[simp]
            theorem Submonoid.fromCommLeftInv_apply {M : Type u_1} [CommMonoid M] (S : Submonoid M) :
            ∀ (a : S.leftInv), S.fromCommLeftInv a = S.fromLeftInv a
            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
              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
              • S.leftNegEquiv hS = { toFun := (↑S.fromCommLeftNeg).toFun, invFun := fun (x : S) => (-IsAddUnit.addUnit ), , left_inv := , right_inv := , map_add' := }
              Instances For
                @[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 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
                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
                • S.leftInvEquiv hS = { toFun := (↑S.fromCommLeftInv).toFun, invFun := fun (x : S) => (IsUnit.unit )⁻¹, , left_inv := , right_inv := , map_mul' := }
                Instances For
                  @[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
                  @[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
                  @[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
                  @[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
                  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.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.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
                  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
                  @[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.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.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.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
                  theorem AddSubmonoid.leftNeg_eq_neg {M : Type u_1} [AddGroup M] (S : AddSubmonoid M) :
                  S.leftNeg = -S
                  theorem Submonoid.leftInv_eq_inv {M : Type u_1} [Group M] (S : Submonoid M) :
                  S.leftInv = S⁻¹
                  @[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.fromLeftInv_eq_inv {M : Type u_1} [Group M] (S : Submonoid M) (x : S.leftInv) :
                  (S.fromLeftInv 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
                  @[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)⁻¹