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]

          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.mem_unop {M : Type u_2} [MulOneClass M] {x : M} {S : Submonoid Mᵐᵒᵖ} :
                  @[simp]
                  @[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]

                  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]
                          @[simp]
                          theorem Submonoid.opEquiv_apply {M : Type u_2} [MulOneClass M] (x : Submonoid M) :
                          @[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] :
                          @[simp]
                          @[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]
                          @[simp]
                          @[simp]
                          @[simp]
                          theorem Submonoid.op_top {M : Type u_2} [MulOneClass M] :
                          @[simp]
                          @[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]
                          @[simp]
                          @[simp]
                          theorem Submonoid.op_sup {M : Type u_2} [MulOneClass M] (S₁ S₂ : Submonoid M) :
                          (S₁S₂).op = S₁.opS₂.op
                          theorem AddSubmonoid.op_sup {M : Type u_2} [AddZeroClass M] (S₁ S₂ : AddSubmonoid M) :
                          (S₁S₂).op = S₁.opS₂.op
                          theorem Submonoid.unop_sup {M : Type u_2} [MulOneClass M] (S₁ S₂ : Submonoid Mᵐᵒᵖ) :
                          (S₁S₂).unop = S₁.unopS₂.unop
                          theorem AddSubmonoid.unop_sup {M : Type u_2} [AddZeroClass M] (S₁ S₂ : AddSubmonoid Mᵃᵒᵖ) :
                          (S₁S₂).unop = S₁.unopS₂.unop
                          theorem Submonoid.op_inf {M : Type u_2} [MulOneClass M] (S₁ S₂ : Submonoid M) :
                          (S₁S₂).op = S₁.opS₂.op
                          theorem AddSubmonoid.op_inf {M : Type u_2} [AddZeroClass M] (S₁ S₂ : AddSubmonoid M) :
                          (S₁S₂).op = S₁.opS₂.op
                          theorem Submonoid.unop_inf {M : Type u_2} [MulOneClass M] (S₁ S₂ : Submonoid Mᵐᵒᵖ) :
                          (S₁S₂).unop = S₁.unopS₂.unop
                          theorem AddSubmonoid.unop_inf {M : Type u_2} [AddZeroClass M] (S₁ S₂ : AddSubmonoid Mᵃᵒᵖ) :
                          (S₁S₂).unop = S₁.unopS₂.unop
                          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) :
                                  @[simp]
                                  theorem AddSubmonoid.equivOp_symm_apply_coe {M : Type u_2} [AddZeroClass M] (H : AddSubmonoid M) (b : H.op) :