Documentation

Iwasawalib.FieldTheory.IntermediateField.MaximalAbelian

Maximal abelian subextension #

"le_lift_XXX_iff" and "lift_XXX_le_iff" are useful results since we often chain these constuctions with IntermediateField.lift.

source
theorem IntermediateField.fixingSubgroup_restrictScalars (K : Type u_3) {L : Type u_4} {L' : Type u_5} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] [Algebra L' L] [IsScalarTower K L' L] [Normal K L] (E : IntermediateField L' L) :
(restrictScalars K E).fixingSubgroup = Subgroup.map (restrictRestrictAlgEquivMapHom K L L' L) E.fixingSubgroup

Unused result. TODO: go mathlib

Maximal abelian subextension #

source
def IntermediateField.maximalAbelianExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] :
IntermediateField F K

The maximal abelian subextension of K / F is the compositum of all abelian subextension of K / F.

Equations
Instances For
    source
    instance IntermediateField.isAbelianGalois_maximalAbelianExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] :
    IsAbelianGalois F ↥(maximalAbelianExtension F K)
    source
    theorem IntermediateField.le_maximalAbelianExtension {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (E : IntermediateField F K) [IsAbelianGalois F ↥E] :
    E ≤ maximalAbelianExtension F K
    source
    theorem IntermediateField.le_maximalAbelianExtension_iff {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (E : IntermediateField F K) :
    E ≤ maximalAbelianExtension F K ↔ IsAbelianGalois F ↥E
    source
    theorem IntermediateField.maximalAbelianExtension_le_iff {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (E : IntermediateField F K) :
    maximalAbelianExtension F K ≤ E ↔ ∀ (E' : IntermediateField F K), IsAbelianGalois F ↥E' → E' ≤ E
    source
    theorem IntermediateField.le_lift_maximalAbelianExtension_iff {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (L E : IntermediateField F K) :
    E ≤ lift (maximalAbelianExtension F ↥L) ↔ E ≤ L ∧ IsAbelianGalois F ↥E
    source
    theorem IntermediateField.lift_maximalAbelianExtension_le_iff {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (L E : IntermediateField F K) :
    lift (maximalAbelianExtension F ↥L) ≤ E ↔ ∀ E' ≤ L, IsAbelianGalois F ↥E' → E' ≤ E
    source
    theorem IntermediateField.maximalAbelianExtension_eq_top (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [IsAbelianGalois F K] :
    maximalAbelianExtension F K = ⊤
    source
    theorem IntermediateField.maximalAbelianExtension_eq_top_iff {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] :
    maximalAbelianExtension F K = ⊤ ↔ IsAbelianGalois F K
    source
    theorem IntermediateField.sup_le_maximalAbelianExtension {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] {E1 E2 : IntermediateField F K} (h1 : E1 ≤ maximalAbelianExtension F K) (h2 : E2 ≤ maximalAbelianExtension F K) :
    E1 ⊔ E2 ≤ maximalAbelianExtension F K
    source
    theorem IntermediateField.iSup_le_maximalAbelianExtension {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] {ι : Type u_3} {E : ι → IntermediateField F K} (h : ∀ (i : ι), E i ≤ maximalAbelianExtension F K) :
    ⨆ (i : ι), E i ≤ maximalAbelianExtension F K
    source
    theorem IntermediateField.fixingSubgroup_maximalAbelianExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [IsGalois F K] :
    (maximalAbelianExtension F K).fixingSubgroup = (commutator Gal(K/F)).topologicalClosure
    source
    theorem IntermediateField.fixingSubgroup_maximalAbelianExtension_of_finiteDimensional (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [IsGalois F K] [FiniteDimensional F K] :
    (maximalAbelianExtension F K).fixingSubgroup = commutator Gal(K/F)
    source
    theorem IntermediateField.isGalois_maximalAbelianExtension_of_isGalois (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (L : Type u_3) [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [IsGalois F L] [IsGalois F K] :
    IsGalois F ↥(maximalAbelianExtension K L)

    Suppose L / K / F is a field extension tower, such that L / F and K / F are Galois. Let H / K be the maximal abelian subextension of L / K. Then H / F is also Galois.

    Maximal abelian S-subextension #

    source
    def IntermediateField.maximalAbelianSExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (S : Set ℕ) :
    IntermediateField F K

    The maximal abelian S-subextension of K / F is defined to be the maximal Galois S-subextension of the maximal abelian subextension of K / F.

    Equations
    Instances For
      source
      instance IntermediateField.isAbelianGalois_maximalAbelianSExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (S : Set ℕ) :
      IsAbelianGalois F ↥(maximalAbelianSExtension F K S)
      source
      instance IntermediateField.isSExtension_maximalAbelianSExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (S : Set ℕ) :
      IsSExtension F (↥(maximalAbelianSExtension F K S)) S
      source
      theorem IntermediateField.maximalAbelianSExtension_eq_sSup (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (S : Set ℕ) :
      maximalAbelianSExtension F K S = sSup {E : IntermediateField F K | IsAbelianGalois F ↥E ∧ IsSExtension F (↥E) S}

      The maximal abelian S-subextension of K / F is equal to the compositum of all abelian subextensions E of K / F which are S-extensions.

      source
      theorem IntermediateField.maximalAbelianSExtension_eq_sSup_finiteDimensional (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (S : Set ℕ) :
      maximalAbelianSExtension F K S = sSup {E : IntermediateField F K | FiniteDimensional F ↥E ∧ IsAbelianGalois F ↥E ∧ IsSExtension F (↥E) S}

      The maximal abelian S-subextension of K / F is equal to the compositum of all finite abelian subextensions E of K / F which are S-extensions.

      source
      theorem IntermediateField.le_maximalAbelianSExtension {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (S : Set ℕ) (E : IntermediateField F K) [IsAbelianGalois F ↥E] [IsSExtension F (↥E) S] :
      E ≤ maximalAbelianSExtension F K S
      source
      theorem IntermediateField.le_maximalAbelianSExtension_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) [IsAbelianGalois F ↥E] (h : ∃ (n : ℕ), Module.finrank F ↥E = p ^ n) :
      E ≤ maximalAbelianSExtension F K {p}
      source
      theorem IntermediateField.le_maximalAbelianSExtension_iff {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] {S : Set ℕ} (E : IntermediateField F K) :
      E ≤ maximalAbelianSExtension F K S ↔ IsAbelianGalois F ↥E ∧ IsSExtension F (↥E) S
      source
      theorem IntermediateField.maximalAbelianSExtension_le_iff {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] {S : Set ℕ} (E : IntermediateField F K) :
      maximalAbelianSExtension F K S ≤ E ↔ ∀ (E' : IntermediateField F K), IsAbelianGalois F ↥E' → IsSExtension F (↥E') S → E' ≤ E
      source
      theorem IntermediateField.le_lift_maximalAbelianSExtension {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) [IsAbelianGalois F ↥E] [IsSExtension F (↥E) S] :
      E ≤ lift (maximalAbelianSExtension F (↥L) S)
      source
      theorem IntermediateField.le_lift_maximalAbelianSExtension_iff {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] {S : Set ℕ} (L E : IntermediateField F K) :
      E ≤ lift (maximalAbelianSExtension F (↥L) S) ↔ E ≤ L ∧ IsAbelianGalois F ↥E ∧ IsSExtension F (↥E) S
      source
      theorem IntermediateField.lift_maximalAbelianSExtension_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 (maximalAbelianSExtension F (↥L) S) ≤ E ↔ ∀ E' ≤ L, IsAbelianGalois F ↥E' → IsSExtension F (↥E') S → E' ≤ E
      source
      theorem IntermediateField.lift_maximalAbelianSExtension_eq_sSup {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (S : Set ℕ) (L : IntermediateField F K) :
      lift (maximalAbelianSExtension F (↥L) S) = sSup {E : IntermediateField F K | E ≤ L ∧ IsAbelianGalois F ↥E ∧ IsSExtension F (↥E) S}
      source
      theorem IntermediateField.lift_maximalAbelianSExtension_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 (maximalAbelianSExtension F (↥L) S) = sSup {E : IntermediateField F K | E ≤ L ∧ FiniteDimensional F ↥E ∧ IsAbelianGalois F ↥E ∧ IsSExtension F (↥E) S}
      source
      theorem IntermediateField.maximalAbelianSExtension_le_maximalAbelianExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (S : Set ℕ) :
      maximalAbelianSExtension F K S ≤ maximalAbelianExtension F K
      source
      theorem IntermediateField.maximalAbelianSExtension_le_maximalGaloisSExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (S : Set ℕ) :
      maximalAbelianSExtension F K S ≤ maximalGaloisSExtension F K S
      source
      theorem IntermediateField.maximalAbelianSExtension_eq_maximalGaloisSExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (S : Set ℕ) [IsAbelianGalois F K] :
      maximalAbelianSExtension F K S = maximalGaloisSExtension F K S
      source
      theorem IntermediateField.isGalois_maximalAbelianSExtension_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 ↥(maximalAbelianSExtension 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 abelian S-subextension of L / K. Then H / F is also Galois.

      source
      theorem IntermediateField.exists_finrank_maximalAbelianSExtension_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 ↥(maximalAbelianSExtension F K {p}) = p ^ n