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)
:
Subalgebra R Aᵐᵒᵖ
Pull a subalgebra back to an opposite subalgebra along MulOpposite.unop
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ᵐᵒᵖ)
:
Subalgebra R A
Pull an subalgebra subring back to a subalgebra along MulOpposite.op
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]
theorem
Subalgebra.unop_toSubsemiring
{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ᵐᵒᵖ}
:
@[simp]
theorem
Subalgebra.unop_op
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S : Subalgebra R A)
:
@[simp]
theorem
Subalgebra.op_unop
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S : Subalgebra R Aᵐᵒᵖ)
:
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₁ 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₁ S₂ : 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.opEquiv_apply
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S : Subalgebra R A)
:
@[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ᵐᵒᵖ)
:
theorem
Subalgebra.op_sup
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S₁ S₂ : Subalgebra R A)
:
theorem
Subalgebra.unop_sup
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S₁ S₂ : Subalgebra R Aᵐᵒᵖ)
:
theorem
Subalgebra.op_inf
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S₁ S₂ : Subalgebra R A)
:
theorem
Subalgebra.unop_inf
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S₁ 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)
:
theorem
Subalgebra.unop_adjoin
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(s : Set 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.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)
:
@[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)
:
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.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)
:
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.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)ᵐᵒᵖ)
: