Maximal Galois S-subextension #
Let S be a set of prime numbers. The maximal Galois S-subextension of K / F
(IntermediateField.maximalGaloisSExtension F K S) is defined to be
the compositum of all finite Galois subextensions E of K / F such that the prime factors of
[E : F] is contained in S.
theorem
IntermediateField.exists_finset_of_le_iSup
{F : Type u_3}
[Field F]
{E : Type u_4}
[Field E]
[Algebra F E]
{ι : Type u_5}
{f : ι → IntermediateField F E}
{x : IntermediateField F E}
[FiniteDimensional F ↥x]
(hx : x ≤ ⨆ (i : ι), f i)
:
TODO: go mathlib below IntermediateField.exists_finset_of_mem_iSup
theorem
Nat.primeFactors_prod_eq_biUnion
{ι : Type u_3}
{f : ι → ℕ}
{s : Finset ι}
(h : ∀ i ∈ s, f i ≠ 0)
:
TODO: go mathlib
Assertion that a field extension is S-extension #
IsSExtension F K S is a typeclass asserting that K / F is an S-extension, which means that
for any finite subextension E / F of K / F, the prime factors of [E : F] is contained in S.
Note that this does not exclude the case that K / F is a purely transcendental extension,
which is mathematically not interesting.
- primeFactors_subset_of_intermediateField_of_finiteDimensional (E : IntermediateField F K) [FiniteDimensional F ↥E] : ↑(Module.finrank F ↥E).primeFactors ⊆ S
Instances
theorem
isSExtension_iff
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
(S : Set ℕ)
:
IsSExtension F K S ↔ ∀ (E : IntermediateField F K) [FiniteDimensional F ↥E], ↑(Module.finrank F ↥E).primeFactors ⊆ S
theorem
IsSExtension.primeFactors_subset_of_intermediateField
{F : Type u_1}
{K : Type u_2}
[Field F]
[Field K]
[Algebra F K]
(S : Set ℕ)
(E : IntermediateField F K)
[IsSExtension F K S]
:
↑(Module.finrank F ↥E).primeFactors ⊆ S
theorem
IsSExtension.primeFactors_subset
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
(S : Set ℕ)
[IsSExtension F K S]
:
↑(Module.finrank F K).primeFactors ⊆ S
theorem
isSExtension_iff_of_finiteDimensional
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
(S : Set ℕ)
[FiniteDimensional F K]
:
theorem
isSExtension_singleton_iff_of_finiteDimensional
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
(p : ℕ)
[Fact (Nat.Prime p)]
[FiniteDimensional F K]
:
theorem
IsSExtension.of_equiv_equiv
(S : Set ℕ)
{F : Type u_3}
{E : Type u_4}
[Field F]
[Field E]
[Algebra F E]
{M : Type u_5}
{N : Type u_6}
[Field M]
[Field N]
[Algebra M N]
{f : F ≃+* M}
{g : E ≃+* N}
(hcomp : (algebraMap M N).comp ↑f = (↑g).comp (algebraMap F E))
[IsSExtension F E S]
:
IsSExtension M N S
theorem
IsSExtension.tower_bot
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
(S : Set ℕ)
(L : Type u_3)
[Field L]
[Algebra F L]
[Algebra K L]
[IsScalarTower F K L]
[IsSExtension F L S]
:
IsSExtension F K S
If L / K / F is a field extension tower, L / F is an S-extension,
then K / F is an S-extension.
theorem
IsSExtension.tower_top_of_isAlgebraic
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
(S : Set ℕ)
(L : Type u_3)
[Field L]
[Algebra F L]
[Algebra K L]
[IsScalarTower F K L]
[IsSExtension F L S]
[Algebra.IsAlgebraic F K]
:
IsSExtension K L S
If L / K / F is a field extension tower, L / F is an S-extension, K / F is algebraic,
then L / K is an S-extension.
theorem
IsSExtension.trans_of_isAlgebraic
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
(S : Set ℕ)
(L : Type u_3)
[Field L]
[Algebra F L]
[Algebra K L]
[IsScalarTower F K L]
[IsSExtension F K S]
[IsSExtension K L S]
[Algebra.IsAlgebraic F K]
:
IsSExtension F L S
If L / K / F is a field extension tower, L / K and K / F are S-extensions,
K / F is algebraic, then L / F is an S-extension.
theorem
IsSExtension.of_subset
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
{S : Set ℕ}
[IsSExtension F K S]
{S' : Set ℕ}
(h : S ⊆ S')
:
IsSExtension F K S'
theorem
IntermediateField.eq_sSup_of_isAlgebraic_of_isSExtension
{F : Type u_1}
{K : Type u_2}
[Field F]
[Field K]
[Algebra F K]
(S : Set ℕ)
(L : IntermediateField F K)
[Algebra.IsAlgebraic F ↥L]
[IsSExtension F (↥L) S]
:
If L / F is an algebraic S-extension, then it is the compositum of all
finite S-extensions inside L.
theorem
IntermediateField.eq_sSup_of_isGalois_of_isSExtension
{F : Type u_1}
{K : Type u_2}
[Field F]
[Field K]
[Algebra F K]
(S : Set ℕ)
(L : IntermediateField F K)
[IsGalois F ↥L]
[IsSExtension F (↥L) S]
:
L = sSup {E : IntermediateField F K | E ≤ L ∧ FiniteDimensional F ↥E ∧ IsGalois F ↥E ∧ IsSExtension F (↥E) S}
If L / F is a Galois S-extension, then it is the compositum of all
finite Galois S-extensions inside L.
instance
isSExtension_iSup_of_isGalois
{F : Type u_1}
{K : Type u_2}
[Field F]
[Field K]
[Algebra F K]
(S : Set ℕ)
{ι : Type u_3}
(L : ι → IntermediateField F K)
[∀ (i : ι), IsGalois F ↥(L i)]
[∀ (i : ι), IsSExtension F (↥(L i)) S]
:
IsSExtension F (↥(⨆ (i : ι), L i)) S
Compositum of a family of Galois S-extensions is also an S-extension.
Note that this is not true for non-Galois case.
instance
isSExtension_sup_of_isGalois
{F : Type u_1}
{K : Type u_2}
[Field F]
[Field K]
[Algebra F K]
(S : Set ℕ)
(E1 E2 : IntermediateField F K)
[IsGalois F ↥E1]
[IsGalois F ↥E2]
[IsSExtension F (↥E1) S]
[IsSExtension F (↥E2) S]
:
IsSExtension F (↥(E1 ⊔ E2)) S
Compositum of a two Galois S-extensions is also an S-extension.
Note that this is not true for non-Galois case.
Maximal Galois S-subextension #
def
IntermediateField.maximalGaloisSExtension
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
(S : Set ℕ)
:
The maximal Galois S-subextension of K / F is defined to be the compositum of all
Galois subextensions E of K / F which are S-extensions (IsSExtension).
Equations
- IntermediateField.maximalGaloisSExtension F K S = sSup {E : IntermediateField F K | IsGalois F ↥E ∧ IsSExtension F (↥E) S}
Instances For
theorem
IntermediateField.maximalGaloisSExtension_eq_sSup_finiteDimensional
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
(S : Set ℕ)
:
maximalGaloisSExtension F K S = sSup {E : IntermediateField F K | FiniteDimensional F ↥E ∧ IsGalois F ↥E ∧ IsSExtension F (↥E) S}
The maximal Galois S-subextension of K / F is also equal to the compositum of all
finite Galois subextensions E of K / F which are S-extensions (IsSExtension).
instance
IntermediateField.isSExtension_maximalGaloisSExtension
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
(S : Set ℕ)
:
IsSExtension F (↥(maximalGaloisSExtension F K S)) S
theorem
IntermediateField.le_maximalGaloisSExtension
{F : Type u_1}
{K : Type u_2}
[Field F]
[Field K]
[Algebra F K]
(S : Set ℕ)
(E : IntermediateField F K)
[IsGalois F ↥E]
[IsSExtension F (↥E) S]
:
theorem
IntermediateField.le_maximalGaloisSExtension_singleton
{F : Type u_1}
{K : Type u_2}
[Field F]
[Field K]
[Algebra F K]
{p : ℕ}
[Fact (Nat.Prime p)]
(E : IntermediateField F K)
[IsGalois F ↥E]
(h : ∃ (n : ℕ), Module.finrank F ↥E = p ^ n)
:
theorem
IntermediateField.le_maximalGaloisSExtension_iff_of_isGalois
{F : Type u_1}
{K : Type u_2}
[Field F]
[Field K]
[Algebra F K]
{S : Set ℕ}
(E : IntermediateField F K)
[IsGalois F ↥E]
:
theorem
IntermediateField.maximalGaloisSExtension_le_iff
{F : Type u_1}
{K : Type u_2}
[Field F]
[Field K]
[Algebra F K]
{S : Set ℕ}
(E : IntermediateField F K)
:
maximalGaloisSExtension F K S ≤ E ↔ ∀ (E' : IntermediateField F K), IsGalois F ↥E' → IsSExtension F (↥E') S → E' ≤ E
theorem
IntermediateField.le_lift_maximalGaloisSExtension
{F : Type u_1}
{K : Type u_2}
[Field F]
[Field K]
[Algebra F K]
(S : Set ℕ)
{L E : IntermediateField F K}
(h : E ≤ L)
[IsGalois F ↥E]
[IsSExtension F (↥E) S]
:
theorem
IntermediateField.le_lift_maximalGaloisSExtension_iff_of_isGalois
{F : Type u_1}
{K : Type u_2}
[Field F]
[Field K]
[Algebra F K]
{S : Set ℕ}
(L E : IntermediateField F K)
[IsGalois F ↥E]
:
theorem
IntermediateField.lift_maximalGaloisSExtension_le_iff
{F : Type u_1}
{K : Type u_2}
[Field F]
[Field K]
[Algebra F K]
{S : Set ℕ}
(L E : IntermediateField F K)
:
lift (maximalGaloisSExtension F (↥L) S) ≤ E ↔ ∀ E' ≤ L, IsGalois F ↥E' → IsSExtension F (↥E') S → E' ≤ E
theorem
IntermediateField.lift_maximalGaloisSExtension_eq_sSup
{F : Type u_1}
{K : Type u_2}
[Field F]
[Field K]
[Algebra F K]
(S : Set ℕ)
(L : IntermediateField F K)
:
lift (maximalGaloisSExtension F (↥L) S) = sSup {E : IntermediateField F K | E ≤ L ∧ IsGalois F ↥E ∧ IsSExtension F (↥E) S}
theorem
IntermediateField.lift_maximalGaloisSExtension_eq_sSup_finiteDimensional
{F : Type u_1}
{K : Type u_2}
[Field F]
[Field K]
[Algebra F K]
(S : Set ℕ)
(L : IntermediateField F K)
:
lift (maximalGaloisSExtension F (↥L) S) = sSup {E : IntermediateField F K | E ≤ L ∧ FiniteDimensional F ↥E ∧ IsGalois F ↥E ∧ IsSExtension F (↥E) S}
theorem
IntermediateField.primeFactors_finrank_subset_of_le_maximalGaloisSExtension
{F : Type u_1}
{K : Type u_2}
[Field F]
[Field K]
[Algebra F K]
{S : Set ℕ}
{E : IntermediateField F K}
(h : E ≤ maximalGaloisSExtension F K S)
:
↑(Module.finrank F ↥E).primeFactors ⊆ S
theorem
IntermediateField.exists_finrank_eq_pow_of_le_maximalGaloisSExtension_singleton
{F : Type u_1}
{K : Type u_2}
[Field F]
[Field K]
[Algebra F K]
{p : ℕ}
[Fact (Nat.Prime p)]
{E : IntermediateField F K}
(h : E ≤ maximalGaloisSExtension F K {p})
[FiniteDimensional F ↥E]
:
∃ (n : ℕ), Module.finrank F ↥E = p ^ n
theorem
IntermediateField.le_maximalGaloisSExtension_iff_of_finiteDimensional_of_isGalois
{F : Type u_1}
{K : Type u_2}
[Field F]
[Field K]
[Algebra F K]
{S : Set ℕ}
(E : IntermediateField F K)
[FiniteDimensional F ↥E]
[IsGalois F ↥E]
:
theorem
IntermediateField.isGalois_maximalGaloisSExtension_of_isGalois
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
(S : Set ℕ)
(L : Type u_3)
[Field L]
[Algebra F L]
[Algebra K L]
[IsScalarTower F K L]
[IsGalois F L]
[IsGalois F K]
:
IsGalois F ↥(maximalGaloisSExtension K L S)
Suppose L / K / F is a field extension tower, such that L / F and K / F are Galois.
Let H / K be the maximal Galois S-subextension of L / K. Then H / F is also Galois.
theorem
IntermediateField.exists_finrank_maximalGaloisSExtension_singleton_eq_pow
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
(p : ℕ)
[Fact (Nat.Prime p)]
[FiniteDimensional F K]
:
∃ (n : ℕ), Module.finrank F ↥(maximalGaloisSExtension F K {p}) = p ^ n
theorem
IntermediateField.fixingSubgroup_maximalGaloisSExtension_singleton
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
(p : ℕ)
[Fact (Nat.Prime p)]
[FiniteDimensional F K]
[IsAbelianGalois F K]
:
theorem
IntermediateField.finrank_maximalGaloisSExtension_singleton_top
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
(p : ℕ)
[Fact (Nat.Prime p)]
[FiniteDimensional F K]
[IsAbelianGalois F K]
:
Module.finrank (↥(maximalGaloisSExtension F K {p})) K = Module.finrank F K / p ^ (Module.finrank F K).factorization p
theorem
IntermediateField.finrank_maximalGaloisSExtension_singleton_bot
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
(p : ℕ)
[Fact (Nat.Prime p)]
[FiniteDimensional F K]
[IsAbelianGalois F K]
:
theorem
IntermediateField.maximalGaloisSExtension_singleton_eq_bot_iff
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
(p : ℕ)
[Fact (Nat.Prime p)]
[FiniteDimensional F K]
[IsAbelianGalois F K]
:
theorem
IntermediateField.not_dvd_finrank_maximalGaloisSExtension_singleton_top
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
(p : ℕ)
[Fact (Nat.Prime p)]
[FiniteDimensional F K]
[IsAbelianGalois F K]
: