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
.
@[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
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
@[simp]
theorem
Subalgebra.op_coe
{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}
:
x ∈ S.op ↔ MulOpposite.unop x ∈ S
@[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
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
@[simp]
theorem
Subalgebra.unop_coe
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S : Subalgebra R Aᵐᵒᵖ)
:
@[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
@[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ᵐᵒᵖ}
:
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}
:
@[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}
:
@[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ᵐᵒᵖ}
:
@[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
@[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
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
@[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₁ : Subalgebra R A)
(S₂ : Subalgebra R A)
:
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ᵐᵒᵖ)
:
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)
:
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ᵐᵒᵖ)
:
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.unop_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.unop_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)
:
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ᵐᵒᵖ)
:
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)
:
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ᵐᵒᵖ)
:
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)
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)
@[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
@[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
def
Subalgebra.linearEquivOp
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S : Subalgebra R A)
:
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
@[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), S.algEquivOpMop a = MulOpposite.op (S.addEquivOp a)
@[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)ᵐᵒᵖ), ↑(S.algEquivOpMop.symm a) = MulOpposite.unop ↑(MulOpposite.unop a)
def
Subalgebra.algEquivOpMop
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S : Subalgebra R A)
:
Bijection between a subalgebra S
and MulOpposite
of its opposite.
Equations
- S.algEquivOpMop = { toEquiv := S.ringEquivOpMop.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
@[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)ᵐᵒᵖ), ↑(S.mopAlgEquivOp a) = MulOpposite.op ↑(MulOpposite.unop a)
@[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), S.mopAlgEquivOp.symm a = MulOpposite.op (S.addEquivOp.symm a)
def
Subalgebra.mopAlgEquivOp
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S : Subalgebra R A)
:
Bijection between MulOpposite
of a subalgebra S
and its opposite.
Equations
- S.mopAlgEquivOp = { toEquiv := S.mopRingEquivOp.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
@[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
@[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