9.27 Linearly disjoint… to 9.28 Review

Section9.27 Linearly disjoint extensions#

Section 9.27 of the Stacks Project, Tag 09IC. 3 tags here are carried by 2 declarations of the repository (all in StacksCore) and 7 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09ID, a definition

Tag 09ID in the Stacks Project.

Declarations registered for the tag:

Tag 09IF, a definition

Tag 09IF in the Stacks Project.

Declarations registered for the tag:

Tag 030M, a lemma

Tag 030M in the Stacks Project.

perfectClosure.isGalois, an instance in StacksCore (human-reviewed), declared in StacksCore/FieldTheory/PurelyInseparable/PerfectClosure.lean, line 64. The attribute's comment: “Second part of 2”.

Stacks 030N (second part of 2). For a normal field extension E/F, the extension E over the perfect closure of F in E is Galois.

instance perfectClosure.isGalois [Normal F E] : IsGalois (perfectClosure F E) E

separableClosure_sup_perfectClosure, a theorem in StacksCore (human-reviewed), declared in StacksCore/FieldTheory/PurelyInseparable/PerfectClosure.lean, line 97. The attribute's comment: “Second part of 3”.

Stacks 030N (second part of 3). For a normal field extension E/F, the separable closure and the perfect closure of F in E together generate the whole extension E.

theorem separableClosure_sup_perfectClosure [Normal F E] :
    separableClosure F E ⊔ perfectClosure F E = ⊤

Declarations registered for the tag:

Sources
LeanMax.max · Subalgebra.linearDisjoint_iff_injective · perfectClosure.isGalois · separableClosure_sup_perfectClosure · separableClosure.isPurelyInseparable · perfectClosure · perfectClosure.isPurelyInseparable · separableClosure_inf_perfectClosure

Section9.28 Review#

Section 9.28 of the Stacks Project, Tag 037H. 2 tags here are carried by 2 declarations of the repository (all in StacksCore) and 5 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 030J, a definition

Tag 030J in the Stacks Project.

Declarations registered for the tag:

Tag 031V, a lemma

Tag 031V in the Stacks Project.

Polynomial.Separable.exists_pow_eq_of_coeff, a theorem in StacksCore (human-reviewed), declared in StacksCore/FieldTheory/Separable.lean, line 24. The attribute's comment: “2, without assuming L/K separable”.

Stacks 031V (part 2 — the general statement). Let K be a field of characteristic p > 0, L/K a field extension, and x ∈ L. If f ∈ K[X] satisfies (a) x is a root of f, (b) f is a separable polynomial, and (c) every coefficient of f is a p-th power in K, then x is a p-th power in L.

theorem Polynomial.Separable.exists_pow_eq_of_coeff {p : ℕ}
    {K L : Type*} [Field K] [CharP K p] [Field L] [Algebra K L] {x : L} {f : Polynomial K}
    (h₁ : f.Separable) (h₂ : f.aeval x = 0) (h₃ : ∀ i, ∃ b : K, b ^ p = f.coeff i) :
    ∃ y, y ^ p = x

exists_pow_eq_of_minpoly_coeff_of_separable, a theorem in StacksCore (human-reviewed), declared in StacksCore/FieldTheory/Separable.lean, line 70. The attribute's comment: “1”.

Stacks 031V (part 1). Let K be a field of characteristic p > 0, L/K a separable extension, and x ∈ L. If every coefficient of the minimal polynomial of x over K is a p-th power in K, then x is a p-th power in L.

theorem exists_pow_eq_of_minpoly_coeff_of_separable {p : ℕ}
    {K : Type*} [Field K] [CharP K p] {L : Type*} [Field L] [Algebra K L] [Algebra.IsSeparable K L]
    {x : L} (h₁ : ∀ i, ∃ b : K, b ^ p = (minpoly K x).coeff i) :
    ∃ y, y ^ p = x
Sources
LeanAlgebra.IsAlgebraic · Algebra.IsSeparable · IsPurelyInseparable · Normal · IsGalois · Polynomial.Separable.exists_pow_eq_of_coeff · exists_pow_eq_of_minpoly_coeff_of_separable

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.