The equal-characteristic proof naturally indexes copies of ℤ_[p] by a positive integer prime to p and a residue-field basis vector. This file records that, when the basis is nonempty, this is exactly a countable product.
Positive degrees prime to p, as used in the Iwasawa product.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalFieldTheory.DiscreteValuationFielddef IwasawaDegree (p : ℕ)A prime-to-p degree together with a residue-field basis coordinate.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalFieldTheory.DiscreteValuationFieldabbrev IwasawaIndex (p f : ℕ)The degrees 1 + pk give an infinite sequence of pairwise distinct positive degrees prime to p.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalFieldTheory.DiscreteValuationFielddef iwasawaDegreeEmbedding (p : ℕ) (hp : 0 < p) : ℕ ↪ IwasawaDegree p where
toFun k :=
⟨1 + p * k, by
constructor
· omega
· exact (Nat.coprime_add_mul_left_left 1 p k).2 (by simp)⟩
inj' := by
intro a b h
have hv : 1 + p * a = 1 + p * b := congrArg Subtype.val h
apply Nat.mul_left_cancel hp
exact Nat.add_left_cancel hvThe Iwasawa index is infinite as soon as the finite basis has a vector.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalFieldTheory.DiscreteValuationFieldtheorem infinite_iwasawaIndex (p f : ℕ) (hp : 0 < p) (hf : 0 < f) :
Infinite (IwasawaIndex p f)The index used in the equal-characteristic proof is denumerable.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalFieldTheory.DiscreteValuationFielddef chosenIwasawaIndexEquivNat (p f : ℕ) (hp : 0 < p) (hf : 0 < f) :
IwasawaIndex p f ≃ ℕReindexing the Iwasawa product gives the canonical ℤ_[p]^ℕ, both algebraically and topologically.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalFieldTheory.DiscreteValuationFielddef iwasawaPadicIntProductContinuousAddEquivNat
(p f : ℕ) [Fact p.Prime] (hp : 0 < p) (hf : 0 < f) :
(IwasawaIndex p f → ℤ_[p]) ≃ₜ+ (ℕ → ℤ_[p])