ℤₚ-extension of fields

Main definitions

• IsMvZpExtension: a Prop which asserts that a Galois extension is with Galois group isomorphic to ℤₚᵈ as a topological group.

• IsZpExtension: a Prop which asserts that a Galois extension is with Galois group isomorphic to ℤₚ as a topological group. It is defined as IsMvZpExtension with d = 1, hence it inherits fields of IsMvZpExtension.

Results should be PR into mathlib

theorem PadicInt.surjective_toZModPow {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) : Function.Surjective ⇑(toZModPow n)

Actual contents of the file

structure IsMvZpExtension (p : ℕ) [Fact (Nat.Prime p)] (d : ℕ) (K : Type u) (Kinf : Type v) [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] : Prop

A Galois extension K∞ / K ia called a ℤₚᵈ-extension, if its Galois group is isomorphic to ℤₚᵈ as a topological group.

• nonempty_continuousMulEquiv : Nonempty ((Kinf ≃ₐ[K] Kinf) ≃ₜ* Multiplicative (Fin d → ℤ_[p]))

theorem isMvZpExtension_iff (p : ℕ) [Fact (Nat.Prime p)] (d : ℕ) (K : Type u) (Kinf : Type v) [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] : IsMvZpExtension p d K Kinf ↔ Nonempty ((Kinf ≃ₐ[K] Kinf) ≃ₜ* Multiplicative (Fin d → ℤ_[p]))

@[reducible, inline]

abbrev IsMvZpExtension.Γ {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) : Type v

The Galois group Γ := Gal(K∞ / K) of a ℤₚᵈ-extension K∞ / K.

Equations

• H.Γ = (Kinf ≃ₐ[K] Kinf)

noncomputable def IsMvZpExtension.continuousMulEquiv {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) : H.Γ ≃ₜ* Multiplicative (Fin d → ℤ_[p])

A random isomorphism from Γ to ℤₚᵈ.

Equations

• H.continuousMulEquiv = Classical.choice ⋯

instance IsMvZpExtension.commGroup {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) : CommGroup H.Γ

The Γ is commutative.

Equations

• H.commGroup = { toGroup := inferInstanceAs (Group H.Γ), mul_comm := ⋯ }

noncomputable def IsMvZpExtension.Γpow {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (n : ℕ) : OpenSubgroup H.Γ

The open subgroup Γ ^ (p ^ n) of Γ.

Equations

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

theorem IsMvZpExtension.mem_Γpow_iff {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (n : ℕ) (σ : H.Γ) : σ ∈ H.Γpow n ↔ ∃ (τ : H.Γ), σ = τ ^ p ^ n

An element is in Γ ^ (p ^ n) if and only if it is p ^ n-th power of some element.

@[simp]

theorem IsMvZpExtension.Γpow_zero {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) : H.Γpow 0 = ⊤

Γ ^ (p ^ 0) = Γ.

instance IsMvZpExtension.normal {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (G : Subgroup H.Γ) : G.Normal

Any subgroup in Γ is a normal subgroup.

@[simp]

theorem IsMvZpExtension.index_Γpow {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (n : ℕ) : (↑(H.Γpow n)).index = p ^ (n * d)

Γ ^ (p ^ n) is of index p ^ (n * d).

theorem IsMvZpExtension.antitone_Γpow {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) : Antitone H.Γpow

If m ≤ n then Γ ^ (p ^ n) ≤ Γ ^ (p ^ m).

theorem IsMvZpExtension.strictAnti_Γpow {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (hd : d ≠ 0) : StrictAnti H.Γpow

If m < n then Γ ^ (p ^ n) < Γ ^ (p ^ m).

noncomputable def IsMvZpExtension.Kn {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (n : ℕ) : IntermediateField K Kinf

The intermediate field Kₙ of K∞ / K fixed by Γ ^ (p ^ n).

Equations

• H.Kn n = IntermediateField.fixedField ↑(H.Γpow n)

@[simp]

theorem IsMvZpExtension.Kn_zero {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) : H.Kn 0 = ⊥

K₀ = K.

theorem IsMvZpExtension.isGalois {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (K' : IntermediateField K Kinf) : IsGalois K ↥K'

Any intermediate field of K∞ / K is Galois.

instance IsMvZpExtension.isGalois_Kn {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (n : ℕ) : IsGalois K ↥(H.Kn n)

Kₙ / K is Galois.

@[simp]

theorem IsMvZpExtension.fixingSubgroup_Kn {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (n : ℕ) : (H.Kn n).fixingSubgroup = ↑(H.Γpow n)

The fixing subgroup of Kₙ is Γ ^ (p ^ n).

instance IsMvZpExtension.finiteDimensional_Kn {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (n : ℕ) : FiniteDimensional K ↥(H.Kn n)

Kₙ / K is a finite extension.

@[simp]

theorem IsMvZpExtension.finrank_Kn {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (n : ℕ) : Module.finrank K ↥(H.Kn n) = p ^ (n * d)

Kₙ / K is of degree p ^ (n * d).

theorem IsMvZpExtension.monotone_Kn {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) : Monotone H.Kn

If m ≤ n then Kₘ ≤ Kₙ.

theorem IsMvZpExtension.strictMono_Kn {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (hd : d ≠ 0) : StrictMono H.Kn

If m < n then Kₘ < Kₙ.

theorem IsMvZpExtension.closure_eq_Γpow_of_closure_eq {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) {s : Set H.Γ} (h : closure ↑(Subgroup.closure s) = ⊤) (n : ℕ) : closure ↑(Subgroup.closure ((fun (x : H.Γ) => x ^ p ^ n) '' s)) = ↑(H.Γpow n)

If the set s topologically generates Γ, then the set s ^ (p ^ n) topologically generates Γ ^ (p ^ n).

theorem IsMvZpExtension.closure_singleton_eq_Γpow_of_closure_singleton_eq {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) {γ : H.Γ} (h : closure ↑(Subgroup.closure {γ}) = ⊤) (n : ℕ) : closure ↑(Subgroup.closure {γ ^ p ^ n}) = ↑(H.Γpow n)

If γ is a topological generator of Γ, then γ ^ (p ^ n) is a topological generator of Γ ^ (p ^ n).

theorem IsMvZpExtension.nhds_one_hasBasis {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) : (nhds 1).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => ↑(H.Γpow n)

Γ ^ (p ^ n) form a neighborhood basis of 1 in Γ.

theorem IsMvZpExtension.Γpow_le_of_isOpen {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (G : Subgroup H.Γ) (h : IsOpen ↑G) : ∃ (n : ℕ), ↑(H.Γpow n) ≤ G

If G is an open subgroup of Γ, then it contains Γ ^ (p ^ n) for some n.

theorem IsMvZpExtension.le_Kn_of_finite {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (K' : IntermediateField K Kinf) [FiniteDimensional K ↥K'] : ∃ (n : ℕ), K' ≤ H.Kn n

If K' is a finite extension of K contained in K∞, then it's contained in Kₙ for some n.

theorem IsMvZpExtension.finrank_eq_pow_of_finite {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (K' : IntermediateField K Kinf) [FiniteDimensional K ↥K'] : ∃ (n : ℕ), Module.finrank K ↥K' = p ^ n

If K' is a finite extension of K contained in K∞, then [K' : K] = p ^ n for some n.

def IsZpExtension (p : ℕ) [Fact (Nat.Prime p)] (K : Type u) (Kinf : Type v) [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] : Prop

A Galois extension K∞ / K ia called a ℤₚ-extension, if its Galois group is isomorphic to ℤₚ as a topological group.

Equations

• IsZpExtension p K Kinf = IsMvZpExtension p 1 K Kinf

theorem isZpExtension_iff (p : ℕ) [Fact (Nat.Prime p)] (K : Type u) (Kinf : Type v) [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] : IsZpExtension p K Kinf ↔ Nonempty ((Kinf ≃ₐ[K] Kinf) ≃ₜ* Multiplicative ℤ_[p])

theorem IsZpExtension.nonempty_continuousMulEquiv {p : ℕ} [Fact (Nat.Prime p)] {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsZpExtension p K Kinf) : Nonempty (IsMvZpExtension.Γ H ≃ₜ* Multiplicative ℤ_[p])

noncomputable def IsZpExtension.continuousMulEquiv {p : ℕ} [Fact (Nat.Prime p)] {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsZpExtension p K Kinf) : IsMvZpExtension.Γ H ≃ₜ* Multiplicative ℤ_[p]

A random isomorphism from Γ to ℤₚ.

Equations

• H.continuousMulEquiv = Classical.choice ⋯

noncomputable def IsZpExtension.topologicalGenerator {p : ℕ} [Fact (Nat.Prime p)] {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsZpExtension p K Kinf) : IsMvZpExtension.Γ H

A random topological generator γ of Γ.

Equations

• H.topologicalGenerator = H.continuousMulEquiv.symm (Multiplicative.ofAdd 1)

theorem IsZpExtension.topologicalGenerator_spec {p : ℕ} [Fact (Nat.Prime p)] {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsZpExtension p K Kinf) : closure ↑(Subgroup.closure {H.topologicalGenerator}) = ⊤

The γ is a topological generator of Γ.

theorem IsZpExtension.closure_topologicalGenerator_pow_eq {p : ℕ} [Fact (Nat.Prime p)] {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsZpExtension p K Kinf) (n : ℕ) : closure ↑(Subgroup.closure {H.topologicalGenerator ^ p ^ n}) = ↑(IsMvZpExtension.Γpow H n)

The γ ^ (p ^ n) is a topological generator of Γ ^ (p ^ n).

theorem IsZpExtension.index_Γpow {p : ℕ} [Fact (Nat.Prime p)] {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsZpExtension p K Kinf) (n : ℕ) : (↑(IsMvZpExtension.Γpow H n)).index = p ^ n

Γ ^ (p ^ n) is of index p ^ n.

theorem IsZpExtension.finrank_Kn {p : ℕ} [Fact (Nat.Prime p)] {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsZpExtension p K Kinf) (n : ℕ) : Module.finrank K ↥(IsMvZpExtension.Kn H n) = p ^ n

Kₙ / K is of degree p ^ n.

theorem IsZpExtension.eq_Γpow_of_isOpen {p : ℕ} [Fact (Nat.Prime p)] {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsZpExtension p K Kinf) (G : Subgroup (IsMvZpExtension.Γ H)) (h : IsOpen ↑G) : ∃ (n : ℕ), G = ↑(IsMvZpExtension.Γpow H n)

If G is an open subgroup of Γ, then it is equal to Γ ^ (p ^ n) for some n.

theorem IsZpExtension.eq_bot_or_Γpow_of_isClosed {p : ℕ} [Fact (Nat.Prime p)] {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsZpExtension p K Kinf) (G : Subgroup (IsMvZpExtension.Γ H)) (h : IsClosed ↑G) : G = ⊥ ∨ ∃ (n : ℕ), G = ↑(IsMvZpExtension.Γpow H n)

If G is a closed subgroup of Γ, then it is equal to 0 or Γ ^ (p ^ n) for some n.

theorem IsZpExtension.eq_Kn_of_finite {p : ℕ} [Fact (Nat.Prime p)] {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsZpExtension p K Kinf) (K' : IntermediateField K Kinf) [FiniteDimensional K ↥K'] : ∃ (n : ℕ), K' = IsMvZpExtension.Kn H n

If K' is a finite extension of K contained in K∞, then it's equal to Kₙ for some n.

theorem IsZpExtension.eq_top_or_Kn {p : ℕ} [Fact (Nat.Prime p)] {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsZpExtension p K Kinf) (K' : IntermediateField K Kinf) : K' = ⊤ ∨ ∃ (n : ℕ), K' = IsMvZpExtension.Kn H n

If K' is an extension of K contained in K∞, then it's equal to K∞ or Kₙ for some n.

theorem IsZpExtension.eq_top_of_infinite {p : ℕ} [Fact (Nat.Prime p)] {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsZpExtension p K Kinf) (K' : IntermediateField K Kinf) (h : ¬FiniteDimensional K ↥K') : K' = ⊤

If K' is an infinite extension of K contained in K∞, then it's equal to K∞.

theorem IsZpExtension.eq_Kn_of_finrank_eq {p : ℕ} [Fact (Nat.Prime p)] {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsZpExtension p K Kinf) (K' : IntermediateField K Kinf) {n : ℕ} (h : Module.finrank K ↥K' = p ^ n) : K' = IsMvZpExtension.Kn H n

If K' is an extension of K of degree p ^ n contained in K∞, then it's equal to Kₙ.