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 an additive submonoid back to an opposite submonoid along AddOpposite.unop

Equations
  • x.op = { carrier := AddOpposite.unop ⁻¹' x, add_mem' := , zero_mem' := }
Instances For
    theorem AddSubmonoid.op.proof_1 {M : Type u_1} [AddZeroClass M] (x : AddSubmonoid M) :
    ∀ {a b : Mᵃᵒᵖ}, a AddOpposite.unop ⁻¹' xb AddOpposite.unop ⁻¹' xAddOpposite.unop b + AddOpposite.unop a x
    @[simp]
    theorem Submonoid.op_coe {M : Type u_2} [MulOneClass M] (x : Submonoid M) :
    x.op = MulOpposite.unop ⁻¹' x
    @[simp]
    theorem AddSubmonoid.op_coe {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid M) :
    x.op = AddOpposite.unop ⁻¹' x

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

    Equations
    • x.op = { carrier := MulOpposite.unop ⁻¹' x, mul_mem' := , one_mem' := }
    Instances For
      @[simp]
      theorem AddSubmonoid.mem_op {M : Type u_2} [AddZeroClass M] {x : Mᵃᵒᵖ} {S : AddSubmonoid M} :
      @[simp]
      theorem Submonoid.mem_op {M : Type u_2} [MulOneClass M] {x : Mᵐᵒᵖ} {S : Submonoid M} :

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

      Equations
      • x.unop = { carrier := AddOpposite.op ⁻¹' x, add_mem' := , zero_mem' := }
      Instances For
        theorem AddSubmonoid.unop.proof_1 {M : Type u_1} [AddZeroClass M] (x : AddSubmonoid Mᵃᵒᵖ) :
        ∀ {a b : M}, a AddOpposite.op ⁻¹' xb AddOpposite.op ⁻¹' x{ unop' := b } + { unop' := a } x
        @[simp]
        theorem Submonoid.unop_coe {M : Type u_2} [MulOneClass M] (x : Submonoid Mᵐᵒᵖ) :
        x.unop = MulOpposite.op ⁻¹' x
        @[simp]
        theorem AddSubmonoid.unop_coe {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid Mᵃᵒᵖ) :
        x.unop = AddOpposite.op ⁻¹' x

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

        Equations
        • x.unop = { carrier := MulOpposite.op ⁻¹' x, mul_mem' := , one_mem' := }
        Instances For
          @[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.mem_unop {M : Type u_2} [MulOneClass M] {x : M} {S : Submonoid Mᵐᵒᵖ} :
          x S.unop MulOpposite.op x S
          @[simp]
          theorem AddSubmonoid.unop_op {M : Type u_2} [AddZeroClass M] (S : AddSubmonoid M) :
          S.op.unop = S
          @[simp]
          theorem Submonoid.unop_op {M : Type u_2} [MulOneClass M] (S : Submonoid M) :
          S.op.unop = S
          @[simp]
          theorem AddSubmonoid.op_unop {M : Type u_2} [AddZeroClass M] (S : AddSubmonoid Mᵃᵒᵖ) :
          S.unop.op = S
          @[simp]
          theorem Submonoid.op_unop {M : Type u_2} [MulOneClass M] (S : Submonoid Mᵐᵒᵖ) :
          S.unop.op = S

          Lattice results #

          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.op_le_iff {M : Type u_2} [MulOneClass M] {S₁ : Submonoid M} {S₂ : Submonoid Mᵐᵒᵖ} :
          S₁.op S₂ S₁ S₂.unop
          theorem AddSubmonoid.le_op_iff {M : Type u_2} [AddZeroClass M] {S₁ : AddSubmonoid Mᵃᵒᵖ} {S₂ : AddSubmonoid M} :
          S₁ S₂.op S₁.unop S₂
          theorem Submonoid.le_op_iff {M : Type u_2} [MulOneClass M] {S₁ : Submonoid Mᵐᵒᵖ} {S₂ : Submonoid M} :
          S₁ S₂.op S₁.unop S₂
          @[simp]
          theorem AddSubmonoid.op_le_op_iff {M : Type u_2} [AddZeroClass M] {S₁ : AddSubmonoid M} {S₂ : AddSubmonoid M} :
          S₁.op S₂.op S₁ S₂
          @[simp]
          theorem Submonoid.op_le_op_iff {M : Type u_2} [MulOneClass M] {S₁ : Submonoid M} {S₂ : Submonoid M} :
          S₁.op S₂.op S₁ S₂
          @[simp]
          theorem AddSubmonoid.unop_le_unop_iff {M : Type u_2} [AddZeroClass M] {S₁ : AddSubmonoid Mᵃᵒᵖ} {S₂ : AddSubmonoid Mᵃᵒᵖ} :
          S₁.unop S₂.unop S₁ S₂
          @[simp]
          theorem Submonoid.unop_le_unop_iff {M : Type u_2} [MulOneClass M] {S₁ : Submonoid Mᵐᵒᵖ} {S₂ : Submonoid Mᵐᵒᵖ} :
          S₁.unop S₂.unop S₁ S₂

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

          Equations
          • AddSubmonoid.opEquiv = { toFun := AddSubmonoid.op, invFun := AddSubmonoid.unop, left_inv := , right_inv := , map_rel_iff' := }
          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 AddSubmonoid.opEquiv_symm_apply {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid Mᵃᵒᵖ) :
            (RelIso.symm AddSubmonoid.opEquiv) x = x.unop
            @[simp]
            theorem Submonoid.opEquiv_symm_apply {M : Type u_2} [MulOneClass M] (x : Submonoid Mᵐᵒᵖ) :
            (RelIso.symm Submonoid.opEquiv) x = x.unop

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

            Equations
            • Submonoid.opEquiv = { toFun := Submonoid.op, invFun := Submonoid.unop, left_inv := , right_inv := , map_rel_iff' := }
            Instances For
              @[simp]
              theorem AddSubmonoid.op_inj {M : Type u_2} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} :
              S.op = T.op S = T
              @[simp]
              theorem Submonoid.op_inj {M : Type u_2} [MulOneClass M] {S : Submonoid M} {T : Submonoid M} :
              S.op = T.op S = T
              @[simp]
              theorem AddSubmonoid.unop_inj {M : Type u_2} [AddZeroClass M] {S : AddSubmonoid Mᵃᵒᵖ} {T : AddSubmonoid Mᵃᵒᵖ} :
              S.unop = T.unop S = T
              @[simp]
              theorem Submonoid.unop_inj {M : Type u_2} [MulOneClass M] {S : Submonoid Mᵐᵒᵖ} {T : Submonoid Mᵐᵒᵖ} :
              S.unop = T.unop S = T
              @[simp]
              theorem AddSubmonoid.op_bot {M : Type u_2} [AddZeroClass M] :
              .op =
              @[simp]
              theorem Submonoid.op_bot {M : Type u_2} [MulOneClass M] :
              .op =
              @[simp]
              theorem AddSubmonoid.op_eq_bot {M : Type u_2} [AddZeroClass M] {S : AddSubmonoid M} :
              S.op = S =
              @[simp]
              theorem Submonoid.op_eq_bot {M : Type u_2} [MulOneClass M] {S : Submonoid M} :
              S.op = S =
              @[simp]
              theorem AddSubmonoid.unop_bot {M : Type u_2} [AddZeroClass M] :
              .unop =
              @[simp]
              theorem Submonoid.unop_bot {M : Type u_2} [MulOneClass M] :
              .unop =
              @[simp]
              theorem AddSubmonoid.unop_eq_bot {M : Type u_2} [AddZeroClass M] {S : AddSubmonoid Mᵃᵒᵖ} :
              S.unop = S =
              @[simp]
              theorem Submonoid.unop_eq_bot {M : Type u_2} [MulOneClass M] {S : Submonoid Mᵐᵒᵖ} :
              S.unop = S =
              @[simp]
              theorem AddSubmonoid.op_top {M : Type u_2} [AddZeroClass M] :
              .op =
              @[simp]
              theorem Submonoid.op_top {M : Type u_2} [MulOneClass M] :
              .op =
              @[simp]
              theorem AddSubmonoid.op_eq_top {M : Type u_2} [AddZeroClass M] {S : AddSubmonoid M} :
              S.op = S =
              @[simp]
              theorem Submonoid.op_eq_top {M : Type u_2} [MulOneClass M] {S : Submonoid M} :
              S.op = S =
              @[simp]
              theorem AddSubmonoid.unop_top {M : Type u_2} [AddZeroClass M] :
              .unop =
              @[simp]
              theorem Submonoid.unop_top {M : Type u_2} [MulOneClass M] :
              .unop =
              @[simp]
              theorem AddSubmonoid.unop_eq_top {M : Type u_2} [AddZeroClass M] {S : AddSubmonoid Mᵃᵒᵖ} :
              S.unop = S =
              @[simp]
              theorem Submonoid.unop_eq_top {M : Type u_2} [MulOneClass M] {S : Submonoid Mᵐᵒᵖ} :
              S.unop = S =
              theorem AddSubmonoid.op_sup {M : Type u_2} [AddZeroClass M] (S₁ : AddSubmonoid M) (S₂ : AddSubmonoid M) :
              (S₁ S₂).op = S₁.op S₂.op
              theorem Submonoid.op_sup {M : Type u_2} [MulOneClass M] (S₁ : Submonoid M) (S₂ : Submonoid M) :
              (S₁ S₂).op = S₁.op S₂.op
              theorem AddSubmonoid.unop_sup {M : Type u_2} [AddZeroClass M] (S₁ : AddSubmonoid Mᵃᵒᵖ) (S₂ : AddSubmonoid Mᵃᵒᵖ) :
              (S₁ S₂).unop = S₁.unop S₂.unop
              theorem Submonoid.unop_sup {M : Type u_2} [MulOneClass M] (S₁ : Submonoid Mᵐᵒᵖ) (S₂ : Submonoid Mᵐᵒᵖ) :
              (S₁ S₂).unop = S₁.unop S₂.unop
              theorem AddSubmonoid.op_inf {M : Type u_2} [AddZeroClass M] (S₁ : AddSubmonoid M) (S₂ : AddSubmonoid M) :
              (S₁ S₂).op = S₁.op S₂.op
              theorem Submonoid.op_inf {M : Type u_2} [MulOneClass M] (S₁ : Submonoid M) (S₂ : Submonoid M) :
              (S₁ S₂).op = S₁.op S₂.op
              theorem AddSubmonoid.unop_inf {M : Type u_2} [AddZeroClass M] (S₁ : AddSubmonoid Mᵃᵒᵖ) (S₂ : AddSubmonoid Mᵃᵒᵖ) :
              (S₁ S₂).unop = S₁.unop S₂.unop
              theorem Submonoid.unop_inf {M : Type u_2} [MulOneClass M] (S₁ : Submonoid Mᵐᵒᵖ) (S₂ : Submonoid Mᵐᵒᵖ) :
              (S₁ S₂).unop = S₁.unop S₂.unop
              theorem AddSubmonoid.op_sSup {M : Type u_2} [AddZeroClass M] (S : Set (AddSubmonoid M)) :
              (sSup S).op = sSup (AddSubmonoid.unop ⁻¹' S)
              theorem Submonoid.op_sSup {M : Type u_2} [MulOneClass M] (S : Set (Submonoid M)) :
              (sSup S).op = sSup (Submonoid.unop ⁻¹' S)
              theorem AddSubmonoid.unop_sSup {M : Type u_2} [AddZeroClass M] (S : Set (AddSubmonoid Mᵃᵒᵖ)) :
              (sSup S).unop = sSup (AddSubmonoid.op ⁻¹' S)
              theorem Submonoid.unop_sSup {M : Type u_2} [MulOneClass M] (S : Set (Submonoid Mᵐᵒᵖ)) :
              (sSup S).unop = sSup (Submonoid.op ⁻¹' S)
              theorem AddSubmonoid.op_sInf {M : Type u_2} [AddZeroClass M] (S : Set (AddSubmonoid M)) :
              (sInf S).op = sInf (AddSubmonoid.unop ⁻¹' S)
              theorem Submonoid.op_sInf {M : Type u_2} [MulOneClass M] (S : Set (Submonoid M)) :
              (sInf S).op = sInf (Submonoid.unop ⁻¹' S)
              theorem AddSubmonoid.unop_sInf {M : Type u_2} [AddZeroClass M] (S : Set (AddSubmonoid Mᵃᵒᵖ)) :
              (sInf S).unop = sInf (AddSubmonoid.op ⁻¹' S)
              theorem Submonoid.unop_sInf {M : Type u_2} [MulOneClass M] (S : Set (Submonoid Mᵐᵒᵖ)) :
              (sInf S).unop = sInf (Submonoid.op ⁻¹' S)
              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.op_iSup {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ιSubmonoid M) :
              (iSup S).op = ⨆ (i : ι), (S i).op
              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.unop_iSup {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ιSubmonoid Mᵐᵒᵖ) :
              (iSup S).unop = ⨆ (i : ι), (S i).unop
              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.op_iInf {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ιSubmonoid M) :
              (iInf S).op = ⨅ (i : ι), (S i).op
              theorem AddSubmonoid.unop_iInf {ι : Sort u_1} {M : Type u_2} [AddZeroClass M] (S : ιAddSubmonoid Mᵃᵒᵖ) :
              (iInf S).unop = ⨅ (i : ι), (S i).unop
              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.op_closure {M : Type u_2} [AddZeroClass M] (s : Set M) :
              theorem Submonoid.op_closure {M : Type u_2} [MulOneClass M] (s : Set M) :
              (Submonoid.closure s).op = Submonoid.closure (MulOpposite.unop ⁻¹' s)
              theorem Submonoid.unop_closure {M : Type u_2} [MulOneClass M] (s : Set Mᵐᵒᵖ) :
              (Submonoid.closure s).unop = Submonoid.closure (MulOpposite.op ⁻¹' s)
              def AddSubmonoid.equivOp {M : Type u_2} [AddZeroClass M] (H : AddSubmonoid M) :
              { x : M // x H } { x : Mᵃᵒᵖ // x H.op }

              Bijection between an additive submonoid H and its opposite.

              Equations
              • H.equivOp = AddOpposite.opEquiv.subtypeEquiv
              Instances For
                theorem AddSubmonoid.equivOp.proof_1 {M : Type u_1} [AddZeroClass M] (H : AddSubmonoid M) :
                ∀ (x : M), x H x H
                @[simp]
                theorem Submonoid.equivOp_symm_apply_coe {M : Type u_2} [MulOneClass M] (H : Submonoid M) (b : { b : 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 : { b : Mᵃᵒᵖ // b H.op }) :
                (H.equivOp.symm b) = AddOpposite.unop b
                @[simp]
                theorem AddSubmonoid.equivOp_apply_coe {M : Type u_2} [AddZeroClass M] (H : AddSubmonoid M) (a : { a : M // a H }) :
                (H.equivOp a) = AddOpposite.op a
                @[simp]
                theorem Submonoid.equivOp_apply_coe {M : Type u_2} [MulOneClass M] (H : Submonoid M) (a : { a : M // a H }) :
                (H.equivOp a) = MulOpposite.op a
                def Submonoid.equivOp {M : Type u_2} [MulOneClass M] (H : Submonoid M) :
                { x : M // x H } { x : Mᵐᵒᵖ // x H.op }

                Bijection between a submonoid H and its opposite.

                Equations
                • H.equivOp = MulOpposite.opEquiv.subtypeEquiv
                Instances For