Maximal abelian subextension #

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

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

Equations

IntermediateField.maximalAbelianExtension F K = sSup {E : IntermediateField F K | IsAbelianGalois F ↥E}

Instances For

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.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.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

def IntermediateField.extendScalars' {F : Type u_1} {K : Type u_2} [Field F] [Field K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] (E : IntermediateField F L) (algebra_map_mem : ∀ (x : K), (algebraMap K L) x ∈ E) :

IntermediateField K L

TODO: adhoc

Equations

E.extendScalars' algebra_map_mem = E.toSubfield.toIntermediateField algebra_map_mem

Instances For

source

@[simp]

theorem IntermediateField.coe_extendScalars' {F : Type u_1} {K : Type u_2} [Field F] [Field K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] (E : IntermediateField F L) (algebra_map_mem : ∀ (x : K), (algebraMap K L) x ∈ E) :

↑(E.extendScalars' algebra_map_mem) = ↑E

source

@[simp]

theorem IntermediateField.extendScalars'_toSubfield {F : Type u_1} {K : Type u_2} [Field F] [Field K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] (E : IntermediateField F L) (algebra_map_mem : ∀ (x : K), (algebraMap K L) x ∈ E) :

(E.extendScalars' algebra_map_mem).toSubfield = E.toSubfield

source

@[simp]

theorem IntermediateField.mem_extendScalars' {F : Type u_1} {K : Type u_2} [Field F] [Field K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] (E : IntermediateField F L) (algebra_map_mem : ∀ (x : K), (algebraMap K L) x ∈ E) (x : L) :

x ∈ E.extendScalars' algebra_map_mem ↔ x ∈ E

source

@[simp]

theorem IntermediateField.extendScalars'_restrictScalars {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] (E : IntermediateField F L) (algebra_map_mem : ∀ (x : K), (algebraMap K L) x ∈ E) [IsScalarTower F K L] :

restrictScalars F (E.extendScalars' algebra_map_mem) = E

source

noncomputable def IntermediateField.autQuotientEquivAutOfIsGalois {F : Type u_3} {L : Type u_4} [Field F] [Field L] [Algebra F L] (K : IntermediateField F L) [IsGalois F ↥K] [IsGalois F L] :

Gal(L/F) ⧸ K.fixingSubgroup ≃* Gal(↥K/F)

... Similar to IsGalois.normalAutEquivQuotient.

Equations

K.autQuotientEquivAutOfIsGalois = MulEquiv.ofBijective (QuotientGroup.lift K.fixingSubgroup (AlgEquiv.restrictNormalHom ↥K) ⋯) ⋯

Instances For

source

theorem IntermediateField.autQuotientEquivAutOfIsGalois_apply {F : Type u_3} {L : Type u_4} [Field F] [Field L] [Algebra F L] (K : IntermediateField F L) [IsGalois F ↥K] [IsGalois F L] (σ : Gal(L/F)) :

K.autQuotientEquivAutOfIsGalois ↑σ = (AlgEquiv.restrictNormalHom ↥K) σ

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

source

noncomputable def IntermediateField.autEquivAutMapMap {F : Type u_3} {L : Type u_4} [Field F] [Field L] [Algebra F L] {K H : IntermediateField F L} (hle : K ≤ H) [IsGalois F L] [IsGalois ↥K ↥(extendScalars hle)] (σ : Gal(L/F)) :

Gal(↥(extendScalars hle)/↥K) ≃* Gal(↥(extendScalars ⋯)/↥(map (↑σ) K))

If K ≤ H are intermediate fields of L / F, σ ∈ Gal(L/F), then there is a natural isomorphism between Gal(H/K) and Gal(σ(H)/σ(K)) given by conjugation by σ.

Equations

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

Instances For

source

noncomputable def IntermediateField.autEquivAutMapOfIsGalois {F : Type u_3} {L : Type u_4} [Field F] [Field L] [Algebra F L] {K H : IntermediateField F L} (hle : K ≤ H) [IsGalois F L] [IsGalois ↥K ↥(extendScalars hle)] [IsGalois F ↥K] (σ : Gal(L/F)) :

Gal(↥(extendScalars hle)/↥K) ≃* Gal(↥(extendScalars ⋯)/↥K)

Version of autEquivAutMapMap with K / F Galois.

Equations

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

Instances For

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)

If L / K / F is a field extension tower, such that L / F and K / F are Galois, then H / F is also Galois, where H is the maximal abelian subextension of L / K.

Maximal abelian `p`-subextension #

source

def IntermediateField.maximalAbelianPExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (p : ℕ) :

IntermediateField F K

The maximal abelian p-subextension of K / F is the compositum of all abelian subextension of K / F whose degree is a power of p.

Equations

IntermediateField.maximalAbelianPExtension F K p = sSup {E : IntermediateField F K | IsAbelianGalois F ↥E ∧ ∃ (n : ℕ), Module.finrank F ↥E = p ^ n}

Instances For

source

instance IntermediateField.isAbelianGalois_maximalAbelianPExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (p : ℕ) :

IsAbelianGalois F ↥(maximalAbelianPExtension F K p)

source

theorem IntermediateField.le_maximalAbelianPExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (p : ℕ) (E : IntermediateField F K) [IsAbelianGalois F ↥E] (h : ∃ (n : ℕ), Module.finrank F ↥E = p ^ n) :

E ≤ maximalAbelianPExtension F K p

source

theorem IntermediateField.isGalois_maximalAbelianPExtension_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] (p : ℕ) :

IsGalois F ↥(maximalAbelianPExtension K L p)

If L / K / F is a field extension tower, such that L / F and K / F are Galois, then H / F is also Galois, where H is the maximal abelian p-subextension of L / K.

source

theorem IntermediateField.exists_finrank_maximalAbelianPExtension_eq (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 ↥(maximalAbelianPExtension F K p) = p ^ n

source

theorem IntermediateField.fixingSubgroup_maximalAbelianPExtension (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] :

(maximalAbelianPExtension F K p).fixingSubgroup = CommGroup.primeToComponent Gal(K/F) p

source

theorem IntermediateField.finrank_maximalAbelianPExtension_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 (↥(maximalAbelianPExtension F K p)) K = Module.finrank F K / p ^ (Module.finrank F K).factorization p

source

theorem IntermediateField.finrank_maximalAbelianPExtension_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] :

Module.finrank F ↥(maximalAbelianPExtension F K p) = p ^ (Module.finrank F K).factorization p

source

theorem IntermediateField.maximalAbelianPExtension_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] :

maximalAbelianPExtension F K p = ⊥ ↔ ¬p ∣ Module.finrank F K

source

theorem IntermediateField.not_dvd_finrank_maximalAbelianPExtension_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] :

¬p ∣ Module.finrank (↥(maximalAbelianPExtension F K p)) K

Documentation

Iwasawalib.FieldTheory.IntermediateField.MaximalAbelian

Maximal abelian subextension #