LeanPool.BrauerGroupNew.Subfield.Subfield

Imported Lean Pool material for LeanPool.BrauerGroupNew.Subfield.Subfield.

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 : IsMax k) : Module.finrank K D = Module.finrank K ↥k * Module.finrank K ↥k

A maximal subfield of a finite-dimensional central division algebra has square dimension.

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

The centralizer condition for a subfield is equivalent to having square dimension.

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'

The square-dimension condition implies maximality among commutative subalgebras.

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

Maximality among commutative subalgebras implies that the centralizer is the subfield itself.

theorem maxsubfield_of_div_iff (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] [FiniteDimensional K D] [Algebra.IsCentral K D] (L : SubField K D) : (∀ (L' : Subalgebra K D), (∀ x ∈ L', ∀ y ∈ L', x * y = y * x) → L.toSubalgebra ≤ L' → L.toSubalgebra = L') ↔ IsMax L

Maximal subfields of a division algebra are exactly maximal commutative subalgebras.

theorem IsMaxSubfield.ofAlgEquiv (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] [FiniteDimensional K D] [Algebra.IsCentral K D] (L1 L2 : SubField K D) (e : ↥L1 ≃ₐ[K] ↥L2) (hL1 : IsMax L1) : IsMax L2

Algebra equivalences preserve maximality of subfields.