theorem
comm_of_centralizer
(K A : Type u)
[Field K]
[Ring A]
[Algebra K A]
(L : Subalgebra K A)
(hL : ∀ (x y : ↥L), x * y = y * x)
:
L ≤ Subalgebra.centralizer K ↑L
theorem
dim_max_subfield
(K D : Type u)
[Field K]
[DivisionRing D]
[Algebra K D]
[FiniteDimensional K D]
[Algebra.IsCentral K D]
(k : SubField K D)
(hk : IsMaximalSubfield K D k)
:
Module.finrank K D = Module.finrank K ↥k * Module.finrank K ↥k
theorem
cor_two_1to2
(K : Type u)
[Field K]
(A : Type u)
[Ring A]
[Algebra K A]
[FiniteDimensional K A]
[Algebra.IsCentral K A]
[IsSimpleRing A]
(L : SubField K A)
:
Subalgebra.centralizer K ↑L.toSubalgebra = L.toSubalgebra ↔ Module.finrank K A = Module.finrank K ↥L * Module.finrank K ↥L
theorem
cor_two_2to3
(K : Type u)
[Field K]
(A : Type u)
[Ring A]
[Algebra K A]
[FiniteDimensional K A]
[Algebra.IsCentral K A]
[IsSimpleRing A]
(L : SubField K A)
:
Module.finrank K A = Module.finrank K ↥L * Module.finrank K ↥L →
∀ (L' : Subalgebra K A), (∀ x ∈ L', ∀ y ∈ L', x * y = y * x) → L.toSubalgebra ≤ L' → L.toSubalgebra = L'
theorem
cor_two_3to1
(K : Type u)
[Field K]
(A : Type u)
[Ring A]
[Algebra K A]
[FiniteDimensional K A]
[Algebra.IsCentral K A]
[IsSimpleRing A]
(L : SubField K A)
:
(∀ (L' : Subalgebra K A), (∀ x ∈ L', ∀ y ∈ L', x * y = y * x) → L.toSubalgebra ≤ L' → L.toSubalgebra = L') →
Subalgebra.centralizer K ↑L = L.toSubalgebra