Documentation

Mathlib.Algebra.Group.Submonoid.MulOpposite

Submonoid of opposite monoids #

For every monoid M, we construct an equivalence between submonoids of M and that of Mᵐᵒᵖ.

Pull a submonoid back to an opposite submonoid along MulOpposite.unop

Equations
Instances For

    Pull an additive submonoid back to an opposite submonoid along AddOpposite.unop

    Equations
    Instances For
      @[simp]
      theorem Submonoid.coe_op {M : Type u_2} [MulOneClass M] (x : Submonoid M) :
      @[simp]
      theorem AddSubmonoid.coe_op {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid M) :
      @[simp]
      theorem Submonoid.mem_op {M : Type u_2} [MulOneClass M] {x : Mᵐᵒᵖ} {S : Submonoid M} :
      @[simp]
      theorem AddSubmonoid.mem_op {M : Type u_2} [AddZeroClass M] {x : Mᵃᵒᵖ} {S : AddSubmonoid M} :

      Pull an opposite submonoid back to a submonoid along MulOpposite.op

      Equations
      Instances For

        Pull an opposite additive submonoid back to a submonoid along AddOpposite.op

        Equations
        Instances For
          @[simp]
          @[simp]
          theorem Submonoid.coe_unop {M : Type u_2} [MulOneClass M] (x : Submonoid Mᵐᵒᵖ) :
          x.unop = MulOpposite.op ⁻¹' x
          @[simp]
          theorem Submonoid.mem_unop {M : Type u_2} [MulOneClass M] {x : M} {S : Submonoid Mᵐᵒᵖ} :
          x S.unop MulOpposite.op x S
          @[simp]
          theorem AddSubmonoid.mem_unop {M : Type u_2} [AddZeroClass M] {x : M} {S : AddSubmonoid Mᵃᵒᵖ} :
          x S.unop AddOpposite.op x S
          @[simp]
          theorem Submonoid.unop_op {M : Type u_2} [MulOneClass M] (S : Submonoid M) :
          S.op.unop = S
          @[simp]
          theorem AddSubmonoid.unop_op {M : Type u_2} [AddZeroClass M] (S : AddSubmonoid M) :
          S.op.unop = S
          @[simp]
          theorem Submonoid.op_unop {M : Type u_2} [MulOneClass M] (S : Submonoid Mᵐᵒᵖ) :
          S.unop.op = S
          @[simp]
          theorem AddSubmonoid.op_unop {M : Type u_2} [AddZeroClass M] (S : AddSubmonoid Mᵃᵒᵖ) :
          S.unop.op = S

          Lattice results #

          theorem Submonoid.op_le_iff {M : Type u_2} [MulOneClass M] {S₁ : Submonoid M} {S₂ : Submonoid Mᵐᵒᵖ} :
          S₁.op S₂ S₁ S₂.unop
          theorem AddSubmonoid.op_le_iff {M : Type u_2} [AddZeroClass M] {S₁ : AddSubmonoid M} {S₂ : AddSubmonoid Mᵃᵒᵖ} :
          S₁.op S₂ S₁ S₂.unop
          theorem Submonoid.le_op_iff {M : Type u_2} [MulOneClass M] {S₁ : Submonoid Mᵐᵒᵖ} {S₂ : Submonoid M} :
          S₁ S₂.op S₁.unop S₂
          theorem AddSubmonoid.le_op_iff {M : Type u_2} [AddZeroClass M] {S₁ : AddSubmonoid Mᵃᵒᵖ} {S₂ : AddSubmonoid M} :
          S₁ S₂.op S₁.unop S₂
          @[simp]
          theorem Submonoid.op_le_op_iff {M : Type u_2} [MulOneClass M] {S₁ S₂ : Submonoid M} :
          S₁.op S₂.op S₁ S₂
          @[simp]
          theorem AddSubmonoid.op_le_op_iff {M : Type u_2} [AddZeroClass M] {S₁ S₂ : AddSubmonoid M} :
          S₁.op S₂.op S₁ S₂
          @[simp]
          theorem Submonoid.unop_le_unop_iff {M : Type u_2} [MulOneClass M] {S₁ S₂ : Submonoid Mᵐᵒᵖ} :
          S₁.unop S₂.unop S₁ S₂
          @[simp]
          theorem AddSubmonoid.unop_le_unop_iff {M : Type u_2} [AddZeroClass M] {S₁ S₂ : AddSubmonoid Mᵃᵒᵖ} :
          S₁.unop S₂.unop S₁ S₂

          A submonoid H of G determines a submonoid H.op of the opposite group Gᵐᵒᵖ.

          Equations
          Instances For

            A additive submonoid H of G determines an additive submonoid H.op of the opposite group Gᵐᵒᵖ.

            Equations
            Instances For
              @[simp]
              theorem AddSubmonoid.opEquiv_apply {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid M) :
              AddSubmonoid.opEquiv x = x.op
              @[simp]
              theorem Submonoid.opEquiv_apply {M : Type u_2} [MulOneClass M] (x : Submonoid M) :
              Submonoid.opEquiv x = x.op
              @[simp]
              theorem Submonoid.op_inj {M : Type u_2} [MulOneClass M] {S T : Submonoid M} :
              S.op = T.op S = T
              @[simp]
              theorem AddSubmonoid.op_inj {M : Type u_2} [AddZeroClass M] {S T : AddSubmonoid M} :
              S.op = T.op S = T
              @[simp]
              theorem Submonoid.unop_inj {M : Type u_2} [MulOneClass M] {S T : Submonoid Mᵐᵒᵖ} :
              S.unop = T.unop S = T
              @[simp]
              theorem AddSubmonoid.unop_inj {M : Type u_2} [AddZeroClass M] {S T : AddSubmonoid Mᵃᵒᵖ} :
              S.unop = T.unop S = T
              @[simp]
              theorem Submonoid.op_bot {M : Type u_2} [MulOneClass M] :
              .op =
              @[simp]
              theorem AddSubmonoid.op_bot {M : Type u_2} [AddZeroClass M] :
              .op =
              @[simp]
              theorem Submonoid.op_eq_bot {M : Type u_2} [MulOneClass M] {S : Submonoid M} :
              S.op = S =
              @[simp]
              theorem AddSubmonoid.op_eq_bot {M : Type u_2} [AddZeroClass M] {S : AddSubmonoid M} :
              S.op = S =
              @[simp]
              theorem Submonoid.unop_bot {M : Type u_2} [MulOneClass M] :
              .unop =
              @[simp]
              theorem AddSubmonoid.unop_bot {M : Type u_2} [AddZeroClass M] :
              .unop =
              @[simp]
              theorem Submonoid.unop_eq_bot {M : Type u_2} [MulOneClass M] {S : Submonoid Mᵐᵒᵖ} :
              S.unop = S =
              @[simp]
              theorem AddSubmonoid.unop_eq_bot {M : Type u_2} [AddZeroClass M] {S : AddSubmonoid Mᵃᵒᵖ} :
              S.unop = S =
              @[simp]
              theorem Submonoid.op_top {M : Type u_2} [MulOneClass M] :
              .op =
              @[simp]
              theorem AddSubmonoid.op_top {M : Type u_2} [AddZeroClass M] :
              .op =
              @[simp]
              theorem Submonoid.op_eq_top {M : Type u_2} [MulOneClass M] {S : Submonoid M} :
              S.op = S =
              @[simp]
              theorem AddSubmonoid.op_eq_top {M : Type u_2} [AddZeroClass M] {S : AddSubmonoid M} :
              S.op = S =
              @[simp]
              theorem Submonoid.unop_top {M : Type u_2} [MulOneClass M] :
              .unop =
              @[simp]
              theorem AddSubmonoid.unop_top {M : Type u_2} [AddZeroClass M] :
              .unop =
              @[simp]
              theorem Submonoid.unop_eq_top {M : Type u_2} [MulOneClass M] {S : Submonoid Mᵐᵒᵖ} :
              S.unop = S =
              @[simp]
              theorem AddSubmonoid.unop_eq_top {M : Type u_2} [AddZeroClass M] {S : AddSubmonoid Mᵃᵒᵖ} :
              S.unop = S =
              theorem Submonoid.op_sup {M : Type u_2} [MulOneClass M] (S₁ S₂ : Submonoid M) :
              (S₁ S₂).op = S₁.op S₂.op
              theorem AddSubmonoid.op_sup {M : Type u_2} [AddZeroClass M] (S₁ S₂ : AddSubmonoid M) :
              (S₁ S₂).op = S₁.op S₂.op
              theorem Submonoid.unop_sup {M : Type u_2} [MulOneClass M] (S₁ S₂ : Submonoid Mᵐᵒᵖ) :
              (S₁ S₂).unop = S₁.unop S₂.unop
              theorem AddSubmonoid.unop_sup {M : Type u_2} [AddZeroClass M] (S₁ S₂ : AddSubmonoid Mᵃᵒᵖ) :
              (S₁ S₂).unop = S₁.unop S₂.unop
              theorem Submonoid.op_inf {M : Type u_2} [MulOneClass M] (S₁ S₂ : Submonoid M) :
              (S₁ S₂).op = S₁.op S₂.op
              theorem AddSubmonoid.op_inf {M : Type u_2} [AddZeroClass M] (S₁ S₂ : AddSubmonoid M) :
              (S₁ S₂).op = S₁.op S₂.op
              theorem Submonoid.unop_inf {M : Type u_2} [MulOneClass M] (S₁ S₂ : Submonoid Mᵐᵒᵖ) :
              (S₁ S₂).unop = S₁.unop S₂.unop
              theorem AddSubmonoid.unop_inf {M : Type u_2} [AddZeroClass M] (S₁ S₂ : AddSubmonoid Mᵃᵒᵖ) :
              (S₁ S₂).unop = S₁.unop S₂.unop
              theorem Submonoid.op_sSup {M : Type u_2} [MulOneClass M] (S : Set (Submonoid M)) :
              theorem Submonoid.op_sInf {M : Type u_2} [MulOneClass M] (S : Set (Submonoid M)) :
              theorem Submonoid.op_iSup {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ιSubmonoid M) :
              (iSup S).op = ⨆ (i : ι), (S i).op
              theorem AddSubmonoid.op_iSup {ι : Sort u_1} {M : Type u_2} [AddZeroClass M] (S : ιAddSubmonoid M) :
              (iSup S).op = ⨆ (i : ι), (S i).op
              theorem Submonoid.unop_iSup {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ιSubmonoid Mᵐᵒᵖ) :
              (iSup S).unop = ⨆ (i : ι), (S i).unop
              theorem AddSubmonoid.unop_iSup {ι : Sort u_1} {M : Type u_2} [AddZeroClass M] (S : ιAddSubmonoid Mᵃᵒᵖ) :
              (iSup S).unop = ⨆ (i : ι), (S i).unop
              theorem Submonoid.op_iInf {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ιSubmonoid M) :
              (iInf S).op = ⨅ (i : ι), (S i).op
              theorem AddSubmonoid.op_iInf {ι : Sort u_1} {M : Type u_2} [AddZeroClass M] (S : ιAddSubmonoid M) :
              (iInf S).op = ⨅ (i : ι), (S i).op
              theorem Submonoid.unop_iInf {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ιSubmonoid Mᵐᵒᵖ) :
              (iInf S).unop = ⨅ (i : ι), (S i).unop
              theorem AddSubmonoid.unop_iInf {ι : Sort u_1} {M : Type u_2} [AddZeroClass M] (S : ιAddSubmonoid Mᵃᵒᵖ) :
              (iInf S).unop = ⨅ (i : ι), (S i).unop
              def Submonoid.equivOp {M : Type u_2} [MulOneClass M] (H : Submonoid M) :
              H H.op

              Bijection between a submonoid H and its opposite.

              Equations
              Instances For
                def AddSubmonoid.equivOp {M : Type u_2} [AddZeroClass M] (H : AddSubmonoid M) :
                H H.op

                Bijection between an additive submonoid H and its opposite.

                Equations
                Instances For
                  @[simp]
                  theorem Submonoid.equivOp_apply_coe {M : Type u_2} [MulOneClass M] (H : Submonoid M) (a : H) :
                  (H.equivOp a) = MulOpposite.op a
                  @[simp]
                  theorem AddSubmonoid.equivOp_apply_coe {M : Type u_2} [AddZeroClass M] (H : AddSubmonoid M) (a : H) :
                  (H.equivOp a) = AddOpposite.op a
                  @[simp]
                  theorem Submonoid.equivOp_symm_apply_coe {M : Type u_2} [MulOneClass M] (H : Submonoid M) (b : H.op) :
                  (H.equivOp.symm b) = MulOpposite.unop b
                  @[simp]
                  theorem AddSubmonoid.equivOp_symm_apply_coe {M : Type u_2} [AddZeroClass M] (H : AddSubmonoid M) (b : H.op) :
                  (H.equivOp.symm b) = AddOpposite.unop b