Documentation

Mathlib.Algebra.Algebra.Subalgebra.MulOpposite

Subalgebras of opposite rings #

For every ring A over a commutative ring R, we construct an equivalence between subalgebras of A / R and that of Aᵐᵒᵖ / R.

def Subalgebra.op {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :

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

Equations
  • S.op = { toSubsemiring := S.op, algebraMap_mem' := }
Instances For
    @[simp]
    theorem Subalgebra.coe_op {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
    @[simp]
    theorem Subalgebra.op_toSubsemiring {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
    @[simp]
    theorem Subalgebra.mem_op {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] {x : Aᵐᵒᵖ} {S : Subalgebra R A} :
    def Subalgebra.unop {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R Aᵐᵒᵖ) :

    Pull an subalgebra subring back to a subalgebra along MulOpposite.op

    Equations
    • S.unop = { toSubsemiring := S.unop, algebraMap_mem' := }
    Instances For
      @[simp]
      theorem Subalgebra.coe_unop {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R Aᵐᵒᵖ) :
      @[simp]
      @[simp]
      theorem Subalgebra.mem_unop {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] {x : A} {S : Subalgebra R Aᵐᵒᵖ} :
      @[simp]
      theorem Subalgebra.unop_op {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
      S.op.unop = S
      @[simp]
      theorem Subalgebra.op_unop {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R Aᵐᵒᵖ) :
      S.unop.op = S

      Lattice results #

      theorem Subalgebra.op_le_iff {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] {S₁ : Subalgebra R A} {S₂ : Subalgebra R Aᵐᵒᵖ} :
      S₁.op S₂ S₁ S₂.unop
      theorem Subalgebra.le_op_iff {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] {S₁ : Subalgebra R Aᵐᵒᵖ} {S₂ : Subalgebra R A} :
      S₁ S₂.op S₁.unop S₂
      @[simp]
      theorem Subalgebra.op_le_op_iff {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] {S₁ S₂ : Subalgebra R A} :
      S₁.op S₂.op S₁ S₂
      @[simp]
      theorem Subalgebra.unop_le_unop_iff {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] {S₁ S₂ : Subalgebra R Aᵐᵒᵖ} :
      S₁.unop S₂.unop S₁ S₂

      A subalgebra S of A / R determines a subring S.op of the opposite ring Aᵐᵒᵖ / R.

      Equations
      Instances For
        @[simp]
        theorem Subalgebra.opEquiv_apply {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
        @[simp]
        @[simp]
        theorem Subalgebra.op_bot {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] :
        @[simp]
        theorem Subalgebra.unop_bot {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] :
        @[simp]
        theorem Subalgebra.op_top {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] :
        @[simp]
        theorem Subalgebra.unop_top {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] :
        theorem Subalgebra.op_sup {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S₁ S₂ : Subalgebra R A) :
        (S₁ S₂).op = S₁.op S₂.op
        theorem Subalgebra.unop_sup {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S₁ S₂ : Subalgebra R Aᵐᵒᵖ) :
        (S₁ S₂).unop = S₁.unop S₂.unop
        theorem Subalgebra.op_inf {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S₁ S₂ : Subalgebra R A) :
        (S₁ S₂).op = S₁.op S₂.op
        theorem Subalgebra.unop_inf {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S₁ S₂ : Subalgebra R Aᵐᵒᵖ) :
        (S₁ S₂).unop = S₁.unop S₂.unop
        theorem Subalgebra.op_sSup {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Set (Subalgebra R A)) :
        theorem Subalgebra.op_sInf {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Set (Subalgebra R A)) :
        theorem Subalgebra.op_iSup {ι : Sort u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : ιSubalgebra R A) :
        (iSup S).op = ⨆ (i : ι), (S i).op
        theorem Subalgebra.unop_iSup {ι : Sort u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : ιSubalgebra R Aᵐᵒᵖ) :
        (iSup S).unop = ⨆ (i : ι), (S i).unop
        theorem Subalgebra.op_iInf {ι : Sort u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : ιSubalgebra R A) :
        (iInf S).op = ⨅ (i : ι), (S i).op
        theorem Subalgebra.unop_iInf {ι : Sort u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : ιSubalgebra R Aᵐᵒᵖ) :
        (iInf S).unop = ⨅ (i : ι), (S i).unop
        def Subalgebra.linearEquivOp {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
        S ≃ₗ[R] S.op

        Bijection between a subalgebra S and its opposite.

        Equations
        Instances For
          @[simp]
          theorem Subalgebra.linearEquivOp_symm_apply_coe {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (a✝ : S.op) :
          (S.linearEquivOp.symm a✝) = MulOpposite.unop a✝
          @[simp]
          theorem Subalgebra.linearEquivOp_apply_coe {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (a✝ : S.toSubsemiring) :
          (S.linearEquivOp a✝) = MulOpposite.op a✝
          def Subalgebra.algEquivOpMop {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
          S ≃ₐ[R] (↥S.op)ᵐᵒᵖ

          Bijection between a subalgebra S and MulOpposite of its opposite.

          Equations
          Instances For
            @[simp]
            theorem Subalgebra.algEquivOpMop_apply {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (a✝ : S.toSubsemiring) :
            @[simp]
            theorem Subalgebra.algEquivOpMop_symm_apply_coe {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (a✝ : (↥S.op)ᵐᵒᵖ) :
            def Subalgebra.mopAlgEquivOp {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
            (↥S)ᵐᵒᵖ ≃ₐ[R] S.op

            Bijection between MulOpposite of a subalgebra S and its opposite.

            Equations
            Instances For
              @[simp]
              theorem Subalgebra.mopAlgEquivOp_symm_apply {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (a✝ : S.op) :
              @[simp]
              theorem Subalgebra.mopAlgEquivOp_apply_coe {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (a✝ : (↥S.toSubsemiring)ᵐᵒᵖ) :
              @[simp]
              theorem Subalgebra.op_toSubring {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) :
              @[simp]
              theorem Subalgebra.unop_toSubring {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R Aᵐᵒᵖ) :