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ᵐᵒᵖ.

source
def Submonoid.op {M : Type u_2} [MulOneClass M] (x : Submonoid M) :
Submonoid Mᵐᵒᵖ

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

Equations
  • x.op = { carrier := MulOpposite.unop ⁻¹' ↑x, mul_mem' := ⋯, one_mem' := ⋯ }
Instances For
    source
    def AddSubmonoid.op {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid M) :
    AddSubmonoid 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
      source
      theorem AddSubmonoid.op.proof_1 {M : Type u_1} [AddZeroClass M] (x : AddSubmonoid M) :
      ∀ {a b : Mᵃᵒᵖ}, a ∈ AddOpposite.unop ⁻¹' ↑x → b ∈ AddOpposite.unop ⁻¹' ↑x → AddOpposite.unop b + AddOpposite.unop a ∈ x
      source
      @[simp]
      theorem Submonoid.op_coe {M : Type u_2} [MulOneClass M] (x : Submonoid M) :
      ↑x.op = MulOpposite.unop ⁻¹' ↑x
      source
      @[simp]
      theorem AddSubmonoid.op_coe {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid M) :
      ↑x.op = AddOpposite.unop ⁻¹' ↑x
      source
      @[simp]
      theorem Submonoid.mem_op {M : Type u_2} [MulOneClass M] {x : Mᵐᵒᵖ} {S : Submonoid M} :
      x ∈ S.op ↔ MulOpposite.unop x ∈ S
      source
      @[simp]
      theorem AddSubmonoid.mem_op {M : Type u_2} [AddZeroClass M] {x : Mᵃᵒᵖ} {S : AddSubmonoid M} :
      x ∈ S.op ↔ AddOpposite.unop x ∈ S
      source
      def Submonoid.unop {M : Type u_2} [MulOneClass M] (x : Submonoid Mᵐᵒᵖ) :
      Submonoid M

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

      Equations
      • x.unop = { carrier := MulOpposite.op ⁻¹' ↑x, mul_mem' := ⋯, one_mem' := ⋯ }
      Instances For
        source
        def AddSubmonoid.unop {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid Mᵃᵒᵖ) :
        AddSubmonoid 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
          source
          theorem AddSubmonoid.unop.proof_1 {M : Type u_1} [AddZeroClass M] (x : AddSubmonoid Mᵃᵒᵖ) :
          ∀ {a b : M}, a ∈ AddOpposite.op ⁻¹' ↑x → b ∈ AddOpposite.op ⁻¹' ↑x → { unop' := b } + { unop' := a } ∈ x
          source
          theorem AddSubmonoid.unop.proof_2 {M : Type u_1} [AddZeroClass M] (x : AddSubmonoid Mᵃᵒᵖ) :
          0 ∈ x.carrier
          source
          @[simp]
          theorem Submonoid.unop_coe {M : Type u_2} [MulOneClass M] (x : Submonoid Mᵐᵒᵖ) :
          ↑x.unop = MulOpposite.op ⁻¹' ↑x
          source
          @[simp]
          theorem AddSubmonoid.unop_coe {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid Mᵃᵒᵖ) :
          ↑x.unop = AddOpposite.op ⁻¹' ↑x
          source
          @[simp]
          theorem Submonoid.mem_unop {M : Type u_2} [MulOneClass M] {x : M} {S : Submonoid Mᵐᵒᵖ} :
          x ∈ S.unop ↔ MulOpposite.op x ∈ S
          source
          @[simp]
          theorem AddSubmonoid.mem_unop {M : Type u_2} [AddZeroClass M] {x : M} {S : AddSubmonoid Mᵃᵒᵖ} :
          x ∈ S.unop ↔ AddOpposite.op x ∈ S
          source
          @[simp]
          theorem Submonoid.unop_op {M : Type u_2} [MulOneClass M] (S : Submonoid M) :
          S.op.unop = S
          source
          @[simp]
          theorem AddSubmonoid.unop_op {M : Type u_2} [AddZeroClass M] (S : AddSubmonoid M) :
          S.op.unop = S
          source
          @[simp]
          theorem Submonoid.op_unop {M : Type u_2} [MulOneClass M] (S : Submonoid Mᵐᵒᵖ) :
          S.unop.op = S
          source
          @[simp]
          theorem AddSubmonoid.op_unop {M : Type u_2} [AddZeroClass M] (S : AddSubmonoid Mᵃᵒᵖ) :
          S.unop.op = S

          Lattice results #

          source
          theorem Submonoid.op_le_iff {M : Type u_2} [MulOneClass M] {S₁ : Submonoid M} {S₂ : Submonoid Mᵐᵒᵖ} :
          S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
          source
          theorem AddSubmonoid.op_le_iff {M : Type u_2} [AddZeroClass M] {S₁ : AddSubmonoid M} {S₂ : AddSubmonoid Mᵃᵒᵖ} :
          S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
          source
          theorem Submonoid.le_op_iff {M : Type u_2} [MulOneClass M] {S₁ : Submonoid Mᵐᵒᵖ} {S₂ : Submonoid M} :
          S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
          source
          theorem AddSubmonoid.le_op_iff {M : Type u_2} [AddZeroClass M] {S₁ : AddSubmonoid Mᵃᵒᵖ} {S₂ : AddSubmonoid M} :
          S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
          source
          @[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₂
          source
          @[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₂
          source
          @[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₂
          source
          @[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₂
          source
          def Submonoid.opEquiv {M : Type u_2} [MulOneClass M] :
          Submonoid M ≃o Submonoid Mᵐᵒᵖ

          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
            source
            def AddSubmonoid.opEquiv {M : Type u_2} [AddZeroClass M] :
            AddSubmonoid M ≃o AddSubmonoid Mᵃᵒᵖ

            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
              source
              @[simp]
              theorem AddSubmonoid.opEquiv_symm_apply {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid Mᵃᵒᵖ) :
              (RelIso.symm AddSubmonoid.opEquiv) x = x.unop
              source
              @[simp]
              theorem Submonoid.opEquiv_apply {M : Type u_2} [MulOneClass M] (x : Submonoid M) :
              Submonoid.opEquiv x = x.op
              source
              @[simp]
              theorem Submonoid.opEquiv_symm_apply {M : Type u_2} [MulOneClass M] (x : Submonoid Mᵐᵒᵖ) :
              (RelIso.symm Submonoid.opEquiv) x = x.unop
              source
              @[simp]
              theorem AddSubmonoid.opEquiv_apply {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid M) :
              AddSubmonoid.opEquiv x = x.op
              source
              theorem Submonoid.op_injective {M : Type u_2} [MulOneClass M] :
              Function.Injective Submonoid.op
              source
              theorem AddSubmonoid.op_injective {M : Type u_2} [AddZeroClass M] :
              Function.Injective AddSubmonoid.op
              source
              theorem Submonoid.unop_injective {M : Type u_2} [MulOneClass M] :
              Function.Injective Submonoid.unop
              source
              theorem AddSubmonoid.unop_injective {M : Type u_2} [AddZeroClass M] :
              Function.Injective AddSubmonoid.unop
              source
              @[simp]
              theorem Submonoid.op_inj {M : Type u_2} [MulOneClass M] {S : Submonoid M} {T : Submonoid M} :
              S.op = T.op ↔ S = T
              source
              @[simp]
              theorem AddSubmonoid.op_inj {M : Type u_2} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} :
              S.op = T.op ↔ S = T
              source
              @[simp]
              theorem Submonoid.unop_inj {M : Type u_2} [MulOneClass M] {S : Submonoid Mᵐᵒᵖ} {T : Submonoid Mᵐᵒᵖ} :
              S.unop = T.unop ↔ S = T
              source
              @[simp]
              theorem AddSubmonoid.unop_inj {M : Type u_2} [AddZeroClass M] {S : AddSubmonoid Mᵃᵒᵖ} {T : AddSubmonoid Mᵃᵒᵖ} :
              S.unop = T.unop ↔ S = T
              source
              @[simp]
              theorem Submonoid.op_bot {M : Type u_2} [MulOneClass M] :
              ⊥.op = ⊥
              source
              @[simp]
              theorem AddSubmonoid.op_bot {M : Type u_2} [AddZeroClass M] :
              ⊥.op = ⊥
              source
              @[simp]
              theorem Submonoid.op_eq_bot {M : Type u_2} [MulOneClass M] {S : Submonoid M} :
              S.op = ⊥ ↔ S = ⊥
              source
              @[simp]
              theorem AddSubmonoid.op_eq_bot {M : Type u_2} [AddZeroClass M] {S : AddSubmonoid M} :
              S.op = ⊥ ↔ S = ⊥
              source
              @[simp]
              theorem Submonoid.unop_bot {M : Type u_2} [MulOneClass M] :
              ⊥.unop = ⊥
              source
              @[simp]
              theorem AddSubmonoid.unop_bot {M : Type u_2} [AddZeroClass M] :
              ⊥.unop = ⊥
              source
              @[simp]
              theorem Submonoid.unop_eq_bot {M : Type u_2} [MulOneClass M] {S : Submonoid Mᵐᵒᵖ} :
              S.unop = ⊥ ↔ S = ⊥
              source
              @[simp]
              theorem AddSubmonoid.unop_eq_bot {M : Type u_2} [AddZeroClass M] {S : AddSubmonoid Mᵃᵒᵖ} :
              S.unop = ⊥ ↔ S = ⊥
              source
              @[simp]
              theorem Submonoid.op_top {M : Type u_2} [MulOneClass M] :
              ⊤.op = ⊤
              source
              @[simp]
              theorem AddSubmonoid.op_top {M : Type u_2} [AddZeroClass M] :
              ⊤.op = ⊤
              source
              @[simp]
              theorem Submonoid.op_eq_top {M : Type u_2} [MulOneClass M] {S : Submonoid M} :
              S.op = ⊤ ↔ S = ⊤
              source
              @[simp]
              theorem AddSubmonoid.op_eq_top {M : Type u_2} [AddZeroClass M] {S : AddSubmonoid M} :
              S.op = ⊤ ↔ S = ⊤
              source
              @[simp]
              theorem Submonoid.unop_top {M : Type u_2} [MulOneClass M] :
              ⊤.unop = ⊤
              source
              @[simp]
              theorem AddSubmonoid.unop_top {M : Type u_2} [AddZeroClass M] :
              ⊤.unop = ⊤
              source
              @[simp]
              theorem Submonoid.unop_eq_top {M : Type u_2} [MulOneClass M] {S : Submonoid Mᵐᵒᵖ} :
              S.unop = ⊤ ↔ S = ⊤
              source
              @[simp]
              theorem AddSubmonoid.unop_eq_top {M : Type u_2} [AddZeroClass M] {S : AddSubmonoid Mᵃᵒᵖ} :
              S.unop = ⊤ ↔ S = ⊤
              source
              theorem Submonoid.op_sup {M : Type u_2} [MulOneClass M] (S₁ : Submonoid M) (S₂ : Submonoid M) :
              (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
              source
              theorem AddSubmonoid.op_sup {M : Type u_2} [AddZeroClass M] (S₁ : AddSubmonoid M) (S₂ : AddSubmonoid M) :
              (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
              source
              theorem Submonoid.unop_sup {M : Type u_2} [MulOneClass M] (S₁ : Submonoid Mᵐᵒᵖ) (S₂ : Submonoid Mᵐᵒᵖ) :
              (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
              source
              theorem AddSubmonoid.unop_sup {M : Type u_2} [AddZeroClass M] (S₁ : AddSubmonoid Mᵃᵒᵖ) (S₂ : AddSubmonoid Mᵃᵒᵖ) :
              (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
              source
              theorem Submonoid.op_inf {M : Type u_2} [MulOneClass M] (S₁ : Submonoid M) (S₂ : Submonoid M) :
              (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
              source
              theorem AddSubmonoid.op_inf {M : Type u_2} [AddZeroClass M] (S₁ : AddSubmonoid M) (S₂ : AddSubmonoid M) :
              (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
              source
              theorem Submonoid.unop_inf {M : Type u_2} [MulOneClass M] (S₁ : Submonoid Mᵐᵒᵖ) (S₂ : Submonoid Mᵐᵒᵖ) :
              (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
              source
              theorem AddSubmonoid.unop_inf {M : Type u_2} [AddZeroClass M] (S₁ : AddSubmonoid Mᵃᵒᵖ) (S₂ : AddSubmonoid Mᵃᵒᵖ) :
              (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
              source
              theorem Submonoid.op_sSup {M : Type u_2} [MulOneClass M] (S : Set (Submonoid M)) :
              (sSup S).op = sSup (Submonoid.unop ⁻¹' S)
              source
              theorem AddSubmonoid.op_sSup {M : Type u_2} [AddZeroClass M] (S : Set (AddSubmonoid M)) :
              (sSup S).op = sSup (AddSubmonoid.unop ⁻¹' S)
              source
              theorem Submonoid.unop_sSup {M : Type u_2} [MulOneClass M] (S : Set (Submonoid Mᵐᵒᵖ)) :
              (sSup S).unop = sSup (Submonoid.op ⁻¹' S)
              source
              theorem AddSubmonoid.unop_sSup {M : Type u_2} [AddZeroClass M] (S : Set (AddSubmonoid Mᵃᵒᵖ)) :
              (sSup S).unop = sSup (AddSubmonoid.op ⁻¹' S)
              source
              theorem Submonoid.op_sInf {M : Type u_2} [MulOneClass M] (S : Set (Submonoid M)) :
              (sInf S).op = sInf (Submonoid.unop ⁻¹' S)
              source
              theorem AddSubmonoid.op_sInf {M : Type u_2} [AddZeroClass M] (S : Set (AddSubmonoid M)) :
              (sInf S).op = sInf (AddSubmonoid.unop ⁻¹' S)
              source
              theorem Submonoid.unop_sInf {M : Type u_2} [MulOneClass M] (S : Set (Submonoid Mᵐᵒᵖ)) :
              (sInf S).unop = sInf (Submonoid.op ⁻¹' S)
              source
              theorem AddSubmonoid.unop_sInf {M : Type u_2} [AddZeroClass M] (S : Set (AddSubmonoid Mᵃᵒᵖ)) :
              (sInf S).unop = sInf (AddSubmonoid.op ⁻¹' S)
              source
              theorem Submonoid.op_iSup {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ι → Submonoid M) :
              (iSup S).op = ⨆ (i : ι), (S i).op
              source
              theorem AddSubmonoid.op_iSup {ι : Sort u_1} {M : Type u_2} [AddZeroClass M] (S : ι → AddSubmonoid M) :
              (iSup S).op = ⨆ (i : ι), (S i).op
              source
              theorem Submonoid.unop_iSup {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ι → Submonoid Mᵐᵒᵖ) :
              (iSup S).unop = ⨆ (i : ι), (S i).unop
              source
              theorem AddSubmonoid.unop_iSup {ι : Sort u_1} {M : Type u_2} [AddZeroClass M] (S : ι → AddSubmonoid Mᵃᵒᵖ) :
              (iSup S).unop = ⨆ (i : ι), (S i).unop
              source
              theorem Submonoid.op_iInf {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ι → Submonoid M) :
              (iInf S).op = ⨅ (i : ι), (S i).op
              source
              theorem AddSubmonoid.op_iInf {ι : Sort u_1} {M : Type u_2} [AddZeroClass M] (S : ι → AddSubmonoid M) :
              (iInf S).op = ⨅ (i : ι), (S i).op
              source
              theorem Submonoid.unop_iInf {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ι → Submonoid Mᵐᵒᵖ) :
              (iInf S).unop = ⨅ (i : ι), (S i).unop
              source
              theorem AddSubmonoid.unop_iInf {ι : Sort u_1} {M : Type u_2} [AddZeroClass M] (S : ι → AddSubmonoid Mᵃᵒᵖ) :
              (iInf S).unop = ⨅ (i : ι), (S i).unop
              source
              theorem Submonoid.op_closure {M : Type u_2} [MulOneClass M] (s : Set M) :
              (Submonoid.closure s).op = Submonoid.closure (MulOpposite.unop ⁻¹' s)
              source
              theorem AddSubmonoid.op_closure {M : Type u_2} [AddZeroClass M] (s : Set M) :
              (AddSubmonoid.closure s).op = AddSubmonoid.closure (AddOpposite.unop ⁻¹' s)
              source
              theorem Submonoid.unop_closure {M : Type u_2} [MulOneClass M] (s : Set Mᵐᵒᵖ) :
              (Submonoid.closure s).unop = Submonoid.closure (MulOpposite.op ⁻¹' s)
              source
              theorem AddSubmonoid.unop_closure {M : Type u_2} [AddZeroClass M] (s : Set Mᵃᵒᵖ) :
              (AddSubmonoid.closure s).unop = AddSubmonoid.closure (AddOpposite.op ⁻¹' s)
              source
              def Submonoid.equivOp {M : Type u_2} [MulOneClass M] (H : Submonoid M) :
              ↥H ≃ ↥H.op

              Bijection between a submonoid H and its opposite.

              Equations
              • H.equivOp = MulOpposite.opEquiv.subtypeEquiv ⋯
              Instances For
                source
                theorem AddSubmonoid.equivOp.proof_1 {M : Type u_1} [AddZeroClass M] (H : AddSubmonoid M) :
                ∀ (x : M), x ∈ H ↔ x ∈ H
                source
                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
                • H.equivOp = AddOpposite.opEquiv.subtypeEquiv ⋯
                Instances For
                  source
                  @[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
                  source
                  @[simp]
                  theorem AddSubmonoid.equivOp_apply_coe {M : Type u_2} [AddZeroClass M] (H : AddSubmonoid M) (a : ↥H) :
                  ↑(H.equivOp a) = AddOpposite.op ↑a
                  source
                  @[simp]
                  theorem Submonoid.equivOp_apply_coe {M : Type u_2} [MulOneClass M] (H : Submonoid M) (a : ↥H) :
                  ↑(H.equivOp a) = MulOpposite.op ↑a
                  source
                  @[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