LeanPool.BrauerGroupNew.Subfield.Separable #

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

theorem SubField.adjoin_centralizer_mul_comm (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] (L : SubField K D) (a : D) (ha : a ∈ Subalgebra.centralizer K ↑L) (x y : D) :

x ∈ Algebra.adjoin K (↑L ∪ {a}) → y ∈ Algebra.adjoin K (↑L ∪ {a}) → x * y = y * x

source

@[reducible]

def SubField.adjoinCommRing (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] (L : SubField K D) (a : D) (ha : a ∈ Subalgebra.centralizer K ↑L) :

CommRing ↥(Algebra.adjoin K (↑L ∪ {a}))

The commutative ring structure on the algebra generated by adjoining a centralizing element.

Equations

SubField.adjoinCommRing K D L a ha = { toRing := (Algebra.adjoin K (↑L ∪ {a})).toRing, mul_comm := ⋯ }

Instances For

source

instance SubField.adjoin_isDomain (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] (L : SubField K D) (a : D) :

IsDomain ↥(Algebra.adjoin K (↑L ∪ {a}))

source

def SubField.adjoin (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] [FiniteDimensional K D] (L : SubField K D) (a : D) (ha : a ∈ Subalgebra.centralizer K ↑L) :

SubField K D

The subfield generated by a subfield and an element centralizing that subfield.

Equations

SubField.adjoin K D L a ha = { toSubsemiring := (Algebra.adjoin K (↑L ∪ {a})).toSubsemiring, algebraMap_mem' := ⋯, mul_comm := ⋯, exists_inverse := ⋯ }

Instances For

source

@[implicit_reducible]

noncomputable def IsLAlg (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] [FiniteDimensional K D] (L : SubField K D) (a : D) (ha : a ∈ Subalgebra.centralizer K ↑L) :

Algebra ↥L ↥(SubField.adjoin K D L a ha)

The natural algebra structure over a subfield after adjoining a centralizing element.

Equations

IsLAlg K D L a ha = (Subalgebra.inclusion ⋯).toAlgebra' ⋯

Instances For

source

theorem SubField.adjoin_scalarTower (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] [FiniteDimensional K D] (L : SubField K D) (a : D) (ha : a ∈ Subalgebra.centralizer K ↑L) :

IsScalarTower K ↥L ↥(adjoin K D L a ha)

source

theorem SubField.le_centralizer (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] (L : SubField K D) :

L.toSubalgebra ≤ Subalgebra.centralizer K ↑L

source

theorem SubField.adjoin_le_centralizer (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] [FiniteDimensional K D] (L : SubField K D) (a : D) (ha : a ∈ Subalgebra.centralizer K ↑L) :

(adjoin K D L a ha).toSubalgebra ≤ Subalgebra.centralizer K ↑L

source

@[reducible, inline]

abbrev AllSepSubfield (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] :

Set (SubField K D)

The set of subfields of a division algebra that are separable over the center.

Equations

AllSepSubfield K D = {L : SubField K D | Algebra.IsSeparable K ↥L}

Instances For

source

instance instNonemptyElemSubFieldAllSepSubfield (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] :

Nonempty ↑(AllSepSubfield K D)

source

@[implicit_reducible]

instance instPartialOrderElemSubFieldAllSepSubfield (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] :

PartialOrder ↑(AllSepSubfield K D)

Equations

One or more equations did not get rendered due to their size.

source

@[reducible, inline]

noncomputable abbrev iSupChainSepsubfield (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] (c : Set ↑(AllSepSubfield K D)) [Nonempty ↑c] (hc1 : IsChain (fun (x1 x2 : ↑(AllSepSubfield K D)) => x1 ≤ x2) c) :

↑(AllSepSubfield K D)

The supremum of a nonempty chain of separable subfields, as a separable subfield.

Equations

iSupChainSepsubfield K D c hc1 = ⟨let __spread.0 := ⨆ (L : ↑c), (↑↑L).toSubalgebra; { toSubalgebra := __spread.0, mul_comm := ⋯, exists_inverse := ⋯ }, ⋯⟩

Instances For

source

theorem exists_max_sepSub (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] :

∃ (L : ↑(AllSepSubfield K D)), IsMax L

source

theorem Set.centralizer.qsmul_mem (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] (L : Set D) (q : ℚ) (a : D) (ha : a ∈ L.centralizer) :

q • a ∈ L.centralizer

source

@[implicit_reducible]

instance instDivInvMonoidSubtypeMemSubalgebraCentralizerCoeSubField (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] (L : SubField K D) :

DivInvMonoid ↥(Subalgebra.centralizer K ↑L)

Equations

One or more equations did not get rendered due to their size.

source

@[implicit_reducible]

instance instRatCastSubtypeMemSubalgebraCentralizerCoeSubField (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] (L : SubField K D) :

RatCast ↥(Subalgebra.centralizer K ↑L)

Equations

instRatCastSubtypeMemSubalgebraCentralizerCoeSubField K D L = { ratCast := fun (q : ℚ) => ⟨↑q, ⋯⟩ }

source

@[simp]

theorem SubField.centralizer.coe_ratCast (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] (L : SubField K D) (q : ℚ) :

↑↑q = ↑q

source

@[implicit_reducible]

instance instNNRatCastSubtypeMemSubalgebraCentralizerCoeSubField (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] (L : SubField K D) :

NNRatCast ↥(Subalgebra.centralizer K ↑L)

Equations

instNNRatCastSubtypeMemSubalgebraCentralizerCoeSubField K D L = { nnratCast := fun (q : ℚ≥0) => ⟨↑q, ⋯⟩ }

source

@[simp]

theorem SubField.centralizer.nnratCast_eq (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] (L : SubField K D) (q : ℚ≥0) :

↑↑q = ↑q

source

@[implicit_reducible]

instance centralizerSubfieldDiv (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] (L : SubField K D) :

DivisionRing ↥(Subalgebra.centralizer K ↑L)

Equations

One or more equations did not get rendered due to their size.

source

@[implicit_reducible]

noncomputable instance instAlgebraSubtypeMemSubFieldSubalgebraCentralizerCoe (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] (L : SubField K D) :

Algebra ↥L ↥(Subalgebra.centralizer K ↑L)

Equations

One or more equations did not get rendered due to their size.

source

instance instIsScalarTowerSubtypeMemSubFieldSubalgebraCentralizerCoe (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] (L : SubField K D) :

IsScalarTower K ↥L ↥(Subalgebra.centralizer K ↑L)

source

instance instFiniteDimensionalSubtypeMemSubFieldSubalgebraCentralizerCoe (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] [FiniteDimensional K D] (L : SubField K D) :

FiniteDimensional ↥L ↥(Subalgebra.centralizer K ↑L)

source

@[reducible, inline]

noncomputable abbrev ZCLEquivZCLMap (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] (L : SubField K D) :

↥(Subalgebra.center K ↥(Subalgebra.centralizer K ↑L)) ≃ₐ[K] ↥(Subalgebra.map (Subalgebra.centralizer K ↑L).val (Subalgebra.center K ↥(Subalgebra.centralizer K ↑L)))

The center of a centralizer is equivalent to its image in the ambient division algebra.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[reducible, inline]

abbrev SubField.botAdjoin (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] [FiniteDimensional K D] (a : D) :

SubField K D

The subfield generated by one element over the base field.

Equations

SubField.botAdjoin K D a = SubField.adjoin K D ⊥ a ⋯

Instances For

source

@[simp]

theorem SubField.self_mem_botAdjoin (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] [FiniteDimensional K D] (a : D) :

a ∈ botAdjoin K D a

source

theorem SubField.botAdjoin_coe (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] [FiniteDimensional K D] (a : D) :

(botAdjoin K D a).toSubalgebra = K[a]

source

theorem IsSeparable.of_algHom_of_map {F : Type u_1} [Field F] {K : Type u_2} {E : Type u_3} [Field K] [Ring E] [Algebra F K] [Algebra F E] [Nontrivial E] (f : K →ₐ[F] E) {x : K} (h : IsSeparable F (f x)) :

IsSeparable F x

source

theorem exists_sep_masSubfield' (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [FiniteDimensional K D] :

∃ (a : D), IsMax (SubField.botAdjoin K D a) ∧ Algebra.IsSeparable K ↥(SubField.botAdjoin K D a)

source

theorem exists_sep_masSubfield (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [FiniteDimensional K D] :

∃ (L : SubField K D), IsMax L ∧ Algebra.IsSeparable K ↥L

source

theorem exists_sep_splitting (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [FiniteDimensional K D] :

∃ (L : Type u) (x : Field L) (x_1 : Algebra K L) (_ : FiniteDimensional K L), Algebra.IsSeparable K L ∧ isSplit K D L

source

theorem exists_finite_galois_split (K D : Type u) [Field K] [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [FiniteDimensional K D] :

∃ (L : Type u) (x : Field L) (x_1 : Algebra K L) (_ : FiniteDimensional K L), IsGalois K L ∧ isSplit K D L