Documentation

Mathlib.GroupTheory.Submonoid.MulOpposite

Submonoid of opposite monoids #

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

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
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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem AddSubmonoid.op_coe {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid M) :
    ↑(AddSubmonoid.op x) = AddOpposite.unop ⁻¹' ↑x
    source
    @[simp]
    theorem Submonoid.op_coe {M : Type u_2} [MulOneClass M] (x : Submonoid M) :
    ↑(Submonoid.op x) = MulOpposite.unop ⁻¹' ↑x
    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
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem AddSubmonoid.mem_op {M : Type u_2} [AddZeroClass M] {x : Mᵃᵒᵖ} {S : AddSubmonoid M} :
      x ∈ AddSubmonoid.op S ↔ AddOpposite.unop x ∈ S
      source
      @[simp]
      theorem Submonoid.mem_op {M : Type u_2} [MulOneClass M] {x : Mᵐᵒᵖ} {S : Submonoid M} :
      x ∈ Submonoid.op S ↔ MulOpposite.unop x ∈ S
      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
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem AddSubmonoid.unop.proof_2 {M : Type u_1} [AddZeroClass M] (x : AddSubmonoid Mᵃᵒᵖ) :
        0 ∈ x.carrier
        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
        @[simp]
        theorem AddSubmonoid.unop_coe {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid Mᵃᵒᵖ) :
        ↑(AddSubmonoid.unop x) = AddOpposite.op ⁻¹' ↑x
        source
        @[simp]
        theorem Submonoid.unop_coe {M : Type u_2} [MulOneClass M] (x : Submonoid Mᵐᵒᵖ) :
        ↑(Submonoid.unop x) = MulOpposite.op ⁻¹' ↑x
        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
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem AddSubmonoid.mem_unop {M : Type u_2} [AddZeroClass M] {x : M} {S : AddSubmonoid Mᵃᵒᵖ} :
          x ∈ AddSubmonoid.unop S ↔ AddOpposite.op x ∈ S
          source
          @[simp]
          theorem Submonoid.mem_unop {M : Type u_2} [MulOneClass M] {x : M} {S : Submonoid Mᵐᵒᵖ} :
          x ∈ Submonoid.unop S ↔ MulOpposite.op x ∈ S
          source
          @[simp]
          theorem AddSubmonoid.unop_op {M : Type u_2} [AddZeroClass M] (S : AddSubmonoid M) :
          AddSubmonoid.unop (AddSubmonoid.op S) = S
          source
          @[simp]
          theorem Submonoid.unop_op {M : Type u_2} [MulOneClass M] (S : Submonoid M) :
          Submonoid.unop (Submonoid.op S) = S
          source
          @[simp]
          theorem AddSubmonoid.op_unop {M : Type u_2} [AddZeroClass M] (S : AddSubmonoid Mᵃᵒᵖ) :
          AddSubmonoid.op (AddSubmonoid.unop S) = S
          source
          @[simp]
          theorem Submonoid.op_unop {M : Type u_2} [MulOneClass M] (S : Submonoid Mᵐᵒᵖ) :
          Submonoid.op (Submonoid.unop S) = S

          Lattice results #

          source
          theorem AddSubmonoid.op_le_iff {M : Type u_2} [AddZeroClass M] {S₁ : AddSubmonoid M} {S₂ : AddSubmonoid Mᵃᵒᵖ} :
          AddSubmonoid.op S₁ ≤ S₂ ↔ S₁ ≤ AddSubmonoid.unop S₂
          source
          theorem Submonoid.op_le_iff {M : Type u_2} [MulOneClass M] {S₁ : Submonoid M} {S₂ : Submonoid Mᵐᵒᵖ} :
          Submonoid.op S₁ ≤ S₂ ↔ S₁ ≤ Submonoid.unop S₂
          source
          theorem AddSubmonoid.le_op_iff {M : Type u_2} [AddZeroClass M] {S₁ : AddSubmonoid Mᵃᵒᵖ} {S₂ : AddSubmonoid M} :
          S₁ ≤ AddSubmonoid.op S₂ ↔ AddSubmonoid.unop S₁ ≤ S₂
          source
          theorem Submonoid.le_op_iff {M : Type u_2} [MulOneClass M] {S₁ : Submonoid Mᵐᵒᵖ} {S₂ : Submonoid M} :
          S₁ ≤ Submonoid.op S₂ ↔ Submonoid.unop S₁ ≤ S₂
          source
          @[simp]
          theorem AddSubmonoid.op_le_op_iff {M : Type u_2} [AddZeroClass M] {S₁ : AddSubmonoid M} {S₂ : AddSubmonoid M} :
          AddSubmonoid.op S₁ ≤ AddSubmonoid.op S₂ ↔ S₁ ≤ S₂
          source
          @[simp]
          theorem Submonoid.op_le_op_iff {M : Type u_2} [MulOneClass M] {S₁ : Submonoid M} {S₂ : Submonoid M} :
          Submonoid.op S₁ ≤ Submonoid.op S₂ ↔ S₁ ≤ S₂
          source
          @[simp]
          theorem AddSubmonoid.unop_le_unop_iff {M : Type u_2} [AddZeroClass M] {S₁ : AddSubmonoid Mᵃᵒᵖ} {S₂ : AddSubmonoid Mᵃᵒᵖ} :
          AddSubmonoid.unop S₁ ≤ AddSubmonoid.unop S₂ ↔ S₁ ≤ S₂
          source
          @[simp]
          theorem Submonoid.unop_le_unop_iff {M : Type u_2} [MulOneClass M] {S₁ : Submonoid Mᵐᵒᵖ} {S₂ : Submonoid Mᵐᵒᵖ} :
          Submonoid.unop S₁ ≤ Submonoid.unop S₂ ↔ S₁ ≤ S₂
          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
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem Submonoid.opEquiv_symm_apply {M : Type u_2} [MulOneClass M] (x : Submonoid Mᵐᵒᵖ) :
            (RelIso.symm Submonoid.opEquiv) x = Submonoid.unop x
            source
            @[simp]
            theorem AddSubmonoid.opEquiv_symm_apply {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid Mᵃᵒᵖ) :
            (RelIso.symm AddSubmonoid.opEquiv) x = AddSubmonoid.unop x
            source
            @[simp]
            theorem AddSubmonoid.opEquiv_apply {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid M) :
            AddSubmonoid.opEquiv x = AddSubmonoid.op x
            source
            @[simp]
            theorem Submonoid.opEquiv_apply {M : Type u_2} [MulOneClass M] (x : Submonoid M) :
            Submonoid.opEquiv x = Submonoid.op x
            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
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem AddSubmonoid.op_bot {M : Type u_2} [AddZeroClass M] :
              AddSubmonoid.op ⊥ = ⊥
              source
              @[simp]
              theorem Submonoid.op_bot {M : Type u_2} [MulOneClass M] :
              Submonoid.op ⊥ = ⊥
              source
              @[simp]
              theorem AddSubmonoid.unop_bot {M : Type u_2} [AddZeroClass M] :
              AddSubmonoid.unop ⊥ = ⊥
              source
              @[simp]
              theorem Submonoid.unop_bot {M : Type u_2} [MulOneClass M] :
              Submonoid.unop ⊥ = ⊥
              source
              @[simp]
              theorem AddSubmonoid.op_top {M : Type u_2} [AddZeroClass M] :
              AddSubmonoid.op ⊤ = ⊤
              source
              @[simp]
              theorem Submonoid.op_top {M : Type u_2} [MulOneClass M] :
              Submonoid.op ⊤ = ⊤
              source
              @[simp]
              theorem AddSubmonoid.unop_top {M : Type u_2} [AddZeroClass M] :
              AddSubmonoid.unop ⊤ = ⊤
              source
              @[simp]
              theorem Submonoid.unop_top {M : Type u_2} [MulOneClass M] :
              Submonoid.unop ⊤ = ⊤
              source
              theorem AddSubmonoid.op_sup {M : Type u_2} [AddZeroClass M] (S₁ : AddSubmonoid M) (S₂ : AddSubmonoid M) :
              AddSubmonoid.op (S₁ ⊔ S₂) = AddSubmonoid.op S₁ ⊔ AddSubmonoid.op S₂
              source
              theorem Submonoid.op_sup {M : Type u_2} [MulOneClass M] (S₁ : Submonoid M) (S₂ : Submonoid M) :
              Submonoid.op (S₁ ⊔ S₂) = Submonoid.op S₁ ⊔ Submonoid.op S₂
              source
              theorem AddSubmonoid.unop_sup {M : Type u_2} [AddZeroClass M] (S₁ : AddSubmonoid Mᵃᵒᵖ) (S₂ : AddSubmonoid Mᵃᵒᵖ) :
              AddSubmonoid.unop (S₁ ⊔ S₂) = AddSubmonoid.unop S₁ ⊔ AddSubmonoid.unop S₂
              source
              theorem Submonoid.unop_sup {M : Type u_2} [MulOneClass M] (S₁ : Submonoid Mᵐᵒᵖ) (S₂ : Submonoid Mᵐᵒᵖ) :
              Submonoid.unop (S₁ ⊔ S₂) = Submonoid.unop S₁ ⊔ Submonoid.unop S₂
              source
              theorem AddSubmonoid.op_inf {M : Type u_2} [AddZeroClass M] (S₁ : AddSubmonoid M) (S₂ : AddSubmonoid M) :
              AddSubmonoid.op (S₁ ⊓ S₂) = AddSubmonoid.op S₁ ⊓ AddSubmonoid.op S₂
              source
              theorem Submonoid.op_inf {M : Type u_2} [MulOneClass M] (S₁ : Submonoid M) (S₂ : Submonoid M) :
              Submonoid.op (S₁ ⊓ S₂) = Submonoid.op S₁ ⊓ Submonoid.op S₂
              source
              theorem AddSubmonoid.unop_inf {M : Type u_2} [AddZeroClass M] (S₁ : AddSubmonoid Mᵃᵒᵖ) (S₂ : AddSubmonoid Mᵃᵒᵖ) :
              AddSubmonoid.unop (S₁ ⊓ S₂) = AddSubmonoid.unop S₁ ⊓ AddSubmonoid.unop S₂
              source
              theorem Submonoid.unop_inf {M : Type u_2} [MulOneClass M] (S₁ : Submonoid Mᵐᵒᵖ) (S₂ : Submonoid Mᵐᵒᵖ) :
              Submonoid.unop (S₁ ⊓ S₂) = Submonoid.unop S₁ ⊓ Submonoid.unop S₂
              source
              theorem AddSubmonoid.op_sSup {M : Type u_2} [AddZeroClass M] (S : Set (AddSubmonoid M)) :
              AddSubmonoid.op (sSup S) = sSup (AddSubmonoid.unop ⁻¹' S)
              source
              theorem Submonoid.op_sSup {M : Type u_2} [MulOneClass M] (S : Set (Submonoid M)) :
              Submonoid.op (sSup S) = sSup (Submonoid.unop ⁻¹' S)
              source
              theorem AddSubmonoid.unop_sSup {M : Type u_2} [AddZeroClass M] (S : Set (AddSubmonoid Mᵃᵒᵖ)) :
              AddSubmonoid.unop (sSup S) = sSup (AddSubmonoid.op ⁻¹' S)
              source
              theorem Submonoid.unop_sSup {M : Type u_2} [MulOneClass M] (S : Set (Submonoid Mᵐᵒᵖ)) :
              Submonoid.unop (sSup S) = sSup (Submonoid.op ⁻¹' S)
              source
              theorem AddSubmonoid.op_sInf {M : Type u_2} [AddZeroClass M] (S : Set (AddSubmonoid M)) :
              AddSubmonoid.op (sInf S) = sInf (AddSubmonoid.unop ⁻¹' S)
              source
              theorem Submonoid.op_sInf {M : Type u_2} [MulOneClass M] (S : Set (Submonoid M)) :
              Submonoid.op (sInf S) = sInf (Submonoid.unop ⁻¹' S)
              source
              theorem AddSubmonoid.unop_sInf {M : Type u_2} [AddZeroClass M] (S : Set (AddSubmonoid Mᵃᵒᵖ)) :
              AddSubmonoid.unop (sInf S) = sInf (AddSubmonoid.op ⁻¹' S)
              source
              theorem Submonoid.unop_sInf {M : Type u_2} [MulOneClass M] (S : Set (Submonoid Mᵐᵒᵖ)) :
              Submonoid.unop (sInf S) = sInf (Submonoid.op ⁻¹' S)
              source
              theorem AddSubmonoid.op_iSup {ι : Sort u_1} {M : Type u_2} [AddZeroClass M] (S : ι → AddSubmonoid M) :
              AddSubmonoid.op (iSup S) = ⨆ (i : ι), AddSubmonoid.op (S i)
              source
              theorem Submonoid.op_iSup {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ι → Submonoid M) :
              Submonoid.op (iSup S) = ⨆ (i : ι), Submonoid.op (S i)
              source
              theorem AddSubmonoid.unop_iSup {ι : Sort u_1} {M : Type u_2} [AddZeroClass M] (S : ι → AddSubmonoid Mᵃᵒᵖ) :
              AddSubmonoid.unop (iSup S) = ⨆ (i : ι), AddSubmonoid.unop (S i)
              source
              theorem Submonoid.unop_iSup {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ι → Submonoid Mᵐᵒᵖ) :
              Submonoid.unop (iSup S) = ⨆ (i : ι), Submonoid.unop (S i)
              source
              theorem AddSubmonoid.op_iInf {ι : Sort u_1} {M : Type u_2} [AddZeroClass M] (S : ι → AddSubmonoid M) :
              AddSubmonoid.op (iInf S) = ⨅ (i : ι), AddSubmonoid.op (S i)
              source
              theorem Submonoid.op_iInf {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ι → Submonoid M) :
              Submonoid.op (iInf S) = ⨅ (i : ι), Submonoid.op (S i)
              source
              theorem AddSubmonoid.unop_iInf {ι : Sort u_1} {M : Type u_2} [AddZeroClass M] (S : ι → AddSubmonoid Mᵃᵒᵖ) :
              AddSubmonoid.unop (iInf S) = ⨅ (i : ι), AddSubmonoid.unop (S i)
              source
              theorem Submonoid.unop_iInf {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ι → Submonoid Mᵐᵒᵖ) :
              Submonoid.unop (iInf S) = ⨅ (i : ι), Submonoid.unop (S i)
              source
              theorem AddSubmonoid.op_closure {M : Type u_2} [AddZeroClass M] (s : Set M) :
              AddSubmonoid.op (AddSubmonoid.closure s) = AddSubmonoid.closure (AddOpposite.unop ⁻¹' s)
              source
              theorem Submonoid.op_closure {M : Type u_2} [MulOneClass M] (s : Set M) :
              Submonoid.op (Submonoid.closure s) = Submonoid.closure (MulOpposite.unop ⁻¹' s)
              source
              theorem AddSubmonoid.unop_closure {M : Type u_2} [AddZeroClass M] (s : Set Mᵃᵒᵖ) :
              AddSubmonoid.unop (AddSubmonoid.closure s) = AddSubmonoid.closure (AddOpposite.op ⁻¹' s)
              source
              theorem Submonoid.unop_closure {M : Type u_2} [MulOneClass M] (s : Set Mᵐᵒᵖ) :
              Submonoid.unop (Submonoid.closure s) = Submonoid.closure (MulOpposite.op ⁻¹' s)
              source
              def AddSubmonoid.equivOp {M : Type u_2} [AddZeroClass M] (H : AddSubmonoid M) :
              ↥H ≃ ↥(AddSubmonoid.op H)

              Bijection between an additive submonoid H and its opposite.

              Equations
              Instances For
                source
                theorem AddSubmonoid.equivOp.proof_1 {M : Type u_1} [AddZeroClass M] (H : AddSubmonoid M) :
                ∀ (x : M), x ∈ H ↔ x ∈ H
                source
                @[simp]
                theorem AddSubmonoid.equivOp_symm_apply_coe {M : Type u_2} [AddZeroClass M] (H : AddSubmonoid M) (b : { b : Mᵃᵒᵖ // (fun (x : Mᵃᵒᵖ) => x ∈ AddSubmonoid.op H) b }) :
                ↑((AddSubmonoid.equivOp H).symm b) = AddOpposite.unop ↑b
                source
                @[simp]
                theorem Submonoid.equivOp_symm_apply_coe {M : Type u_2} [MulOneClass M] (H : Submonoid M) (b : { b : Mᵐᵒᵖ // (fun (x : Mᵐᵒᵖ) => x ∈ Submonoid.op H) b }) :
                ↑((Submonoid.equivOp H).symm b) = MulOpposite.unop ↑b
                source
                @[simp]
                theorem Submonoid.equivOp_apply_coe {M : Type u_2} [MulOneClass M] (H : Submonoid M) (a : { a : M // (fun (x : M) => x ∈ H) a }) :
                ↑((Submonoid.equivOp H) a) = MulOpposite.op ↑a
                source
                @[simp]
                theorem AddSubmonoid.equivOp_apply_coe {M : Type u_2} [AddZeroClass M] (H : AddSubmonoid M) (a : { a : M // (fun (x : M) => x ∈ H) a }) :
                ↑((AddSubmonoid.equivOp H) a) = AddOpposite.op ↑a
                source
                def Submonoid.equivOp {M : Type u_2} [MulOneClass M] (H : Submonoid M) :
                ↥H ≃ ↥(Submonoid.op H)

                Bijection between a submonoid H and its opposite.

                Equations
                Instances For