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.

source
@[simp]
theorem Subalgebra.op_toSubsemiring {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
S.op.toSubsemiring = S.op
source
def Subalgebra.op {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
Subalgebra R Aᵐᵒᵖ

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

Equations
  • S.op = { toSubsemiring := S.op, algebraMap_mem' := ⋯ }
Instances For
    source
    @[simp]
    theorem Subalgebra.op_coe {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
    ↑S.op = MulOpposite.unop ⁻¹' ↑S
    source
    @[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} :
    x ∈ S.op ↔ MulOpposite.unop x ∈ S
    source
    @[simp]
    theorem Subalgebra.unop_toSubsemiring {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R Aᵐᵒᵖ) :
    S.unop.toSubsemiring = S.unop
    source
    def Subalgebra.unop {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R Aᵐᵒᵖ) :
    Subalgebra R A

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

    Equations
    • S.unop = { toSubsemiring := S.unop, algebraMap_mem' := ⋯ }
    Instances For
      source
      @[simp]
      theorem Subalgebra.unop_coe {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R Aᵐᵒᵖ) :
      ↑S.unop = MulOpposite.op ⁻¹' ↑S
      source
      @[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ᵐᵒᵖ} :
      x ∈ S.unop ↔ MulOpposite.op x ∈ S
      source
      @[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
      source
      @[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 #

      source
      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
      source
      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₂
      source
      @[simp]
      theorem Subalgebra.op_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₁.op ≤ S₂.op ↔ S₁ ≤ S₂
      source
      @[simp]
      theorem Subalgebra.unop_le_unop_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₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
      source
      @[simp]
      theorem Subalgebra.opEquiv_apply {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
      Subalgebra.opEquiv S = S.op
      source
      @[simp]
      theorem Subalgebra.opEquiv_symm_apply {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R Aᵐᵒᵖ) :
      (RelIso.symm Subalgebra.opEquiv) S = S.unop
      source
      def Subalgebra.opEquiv {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] :
      Subalgebra R A ≃o Subalgebra R Aᵐᵒᵖ

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

      Equations
      • Subalgebra.opEquiv = { toFun := Subalgebra.op, invFun := Subalgebra.unop, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
      Instances For
        source
        @[simp]
        theorem Subalgebra.op_bot {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] :
        ⊥.op = ⊥
        source
        @[simp]
        theorem Subalgebra.unop_bot {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] :
        ⊥.unop = ⊥
        source
        @[simp]
        theorem Subalgebra.op_top {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] :
        ⊤.op = ⊤
        source
        @[simp]
        theorem Subalgebra.unop_top {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] :
        ⊤.unop = ⊤
        source
        theorem Subalgebra.op_sup {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₁.op ⊔ S₂.op
        source
        theorem Subalgebra.unop_sup {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₂).unop = S₁.unop ⊔ S₂.unop
        source
        theorem Subalgebra.op_inf {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₁.op ⊓ S₂.op
        source
        theorem Subalgebra.unop_inf {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₂).unop = S₁.unop ⊓ S₂.unop
        source
        theorem Subalgebra.op_sSup {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Set (Subalgebra R A)) :
        (sSup S).op = sSup (Subalgebra.unop ⁻¹' S)
        source
        theorem Subalgebra.unop_sSup {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Set (Subalgebra R Aᵐᵒᵖ)) :
        (sSup S).unop = sSup (Subalgebra.op ⁻¹' S)
        source
        theorem Subalgebra.op_sInf {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Set (Subalgebra R A)) :
        (sInf S).op = sInf (Subalgebra.unop ⁻¹' S)
        source
        theorem Subalgebra.unop_sInf {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Set (Subalgebra R Aᵐᵒᵖ)) :
        (sInf S).unop = sInf (Subalgebra.op ⁻¹' S)
        source
        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
        source
        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
        source
        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
        source
        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
        source
        theorem Subalgebra.op_adjoin {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) :
        (Algebra.adjoin R s).op = Algebra.adjoin R (MulOpposite.unop ⁻¹' s)
        source
        theorem Subalgebra.unop_adjoin {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set Aᵐᵒᵖ) :
        (Algebra.adjoin R s).unop = Algebra.adjoin R (MulOpposite.op ⁻¹' s)
        source
        @[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 : { x : A // x ∈ S.toSubsemiring }), ↑(S.linearEquivOp a) = MulOpposite.op ↑a
        source
        @[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 : { x : Aᵐᵒᵖ // x ∈ S.op }), ↑(S.linearEquivOp.symm a) = MulOpposite.unop ↑a
        source
        def Subalgebra.linearEquivOp {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
        { x : A // x ∈ S } ≃ₗ[R] { x : Aᵐᵒᵖ // x ∈ S.op }

        Bijection between a subalgebra S and its opposite.

        Equations
        • S.linearEquivOp = { toFun := S.addEquivOp.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := S.addEquivOp.invFun, left_inv := ⋯, right_inv := ⋯ }
        Instances For
          source
          @[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 : { x : A // x ∈ S.toSubsemiring }), S.algEquivOpMop a = MulOpposite.op (S.addEquivOp a)
          source
          @[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 : { x : Aᵐᵒᵖ // x ∈ S.op }ᵐᵒᵖ), ↑(S.algEquivOpMop.symm a) = MulOpposite.unop ↑(MulOpposite.unop a)
          source
          def Subalgebra.algEquivOpMop {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
          { x : A // x ∈ S } ≃ₐ[R] { x : Aᵐᵒᵖ // x ∈ S.op }ᵐᵒᵖ

          Bijection between a subalgebra S and MulOpposite of its opposite.

          Equations
          • S.algEquivOpMop = { toEquiv := S.ringEquivOpMop.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
          Instances For
            source
            @[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 : { x : A // x ∈ S.toSubsemiring }ᵐᵒᵖ), ↑(S.mopAlgEquivOp a) = MulOpposite.op ↑(MulOpposite.unop a)
            source
            @[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 : { x : Aᵐᵒᵖ // x ∈ S.op }), S.mopAlgEquivOp.symm a = MulOpposite.op (S.addEquivOp.symm a)
            source
            def Subalgebra.mopAlgEquivOp {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
            { x : A // x ∈ S }ᵐᵒᵖ ≃ₐ[R] { x : Aᵐᵒᵖ // x ∈ S.op }

            Bijection between MulOpposite of a subalgebra S and its opposite.

            Equations
            • S.mopAlgEquivOp = { toEquiv := S.mopRingEquivOp.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
            Instances For
              source
              @[simp]
              theorem Subalgebra.op_toSubring {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) :
              S.op.toSubring = S.toSubring.op
              source
              @[simp]
              theorem Subalgebra.unop_toSubring {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R Aᵐᵒᵖ) :
              S.unop.toSubring = S.toSubring.unop