Documentation

TauCeti.Topology.Algebra.Group.Profinite.ZHat.Component

The ℓ-adic components of the profinite integers #

For a prime ℓ, the ring of profinite integers Additive zHat maps onto the ring of ℓ-adic integers: the projections zHat.toZMod (ℓ ^ k) onto the finite levels ZMod (ℓ ^ k) are compatible along the reduction maps, so Mathlib's inverse-limit universal property of ℤ_[ℓ] (PadicInt.lift) assembles them into a ring homomorphism

zHat.component ℓ : Additive zHat →+* ℤ_[ℓ],

characterized by PadicInt.toZModPow k (zHat.component ℓ a) = zHat.toZMod (ℓ ^ k) a (zHat.toZModPow_component, uniquely by zHat.component_unique).

The same map has a group-theoretic description: read multiplicatively, it is the continuous homomorphism zHat.lift (ofAdd 1) from zHat to the pro-ℓ group Multiplicative ℤ_[ℓ] (zHat.component_apply). Hence the component is continuous and surjective, and Tau Ceti's identification zHat.maximalProPQuotientEquivPadicInt of the maximal pro-ℓ quotient of zHat with ℤ_[ℓ] sends the class of a to zHat.component ℓ a (zHat.maximalProPQuotientEquivPadicInt_mk_eq_component): the ℓ-adic part of the profinite integers has one description, not two.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.zHat.component (ℓ : ℕ) [Fact (Nat.Prime ℓ)] :
Additive ↑zHat.toProfinite.toTop →+* ℤ_[ℓ]

The ℓ-adic component of a profinite integer. The projections of Additive zHat onto the levels ZMod (ℓ ^ k) are compatible along the reduction maps, so the inverse-limit universal property of ℤ_[ℓ] (PadicInt.lift) assembles them into a ring homomorphism Additive zHat →+* ℤ_[ℓ]. It is characterized by zHat.toZModPow_component.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.zHat.toZModPow_component (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (k : ℕ) (a : Additive ↑zHat.toProfinite.toTop) :
    (PadicInt.toZModPow k) ((component ℓ) a) = (toZMod ⟨ℓ ^ k, ⋯⟩) a

    The characterizing equation of the component. Reducing the ℓ-adic component of a modulo ℓ ^ k is reducing a modulo ℓ ^ k.

    source
    theorem TauCeti.zHat.toZModPow_comp_component (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (k : ℕ) :
    (PadicInt.toZModPow k).comp (component ℓ) = toZMod ⟨ℓ ^ k, ⋯⟩

    The characterizing equation of the component, as an equality of ring homomorphisms.

    source
    theorem TauCeti.zHat.component_unique (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (g : Additive ↑zHat.toProfinite.toTop →+* ℤ_[ℓ]) (hg : ∀ (k : ℕ), (PadicInt.toZModPow k).comp g = toZMod ⟨ℓ ^ k, ⋯⟩) :
    g = component ℓ

    Uniqueness of the component. A ring homomorphism Additive zHat →+* ℤ_[ℓ] whose reduction modulo every ℓ ^ k is reduction modulo ℓ ^ k is the component.

    source
    theorem TauCeti.zHat.component_apply (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (a : Additive ↑zHat.toProfinite.toTop) :
    (component ℓ) a = Multiplicative.toAdd ((lift (Multiplicative.ofAdd 1)) (Additive.toMul a))

    The component is the lift of 1 ∈ ℤ_[ℓ]. Read multiplicatively, the ℓ-adic component is the continuous homomorphism from zHat to Multiplicative ℤ_[ℓ] sending the generator to ofAdd 1.

    source
    @[simp]
    theorem TauCeti.zHat.lift_ofAdd_one_padicInt_apply (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (x : ↑zHat.toProfinite.toTop) :
    (lift (Multiplicative.ofAdd 1)) x = Multiplicative.ofAdd ((component ℓ) (Additive.ofMul x))

    The lift of 1 ∈ ℤ_[ℓ] from zHat to Multiplicative ℤ_[ℓ] is the ℓ-adic component, read multiplicatively.

    source
    theorem TauCeti.zHat.continuous_component (ℓ : ℕ) [Fact (Nat.Prime ℓ)] :
    Continuous ⇑(component ℓ)

    The ℓ-adic component is continuous.

    source
    theorem TauCeti.zHat.maximalProPQuotientEquivPadicInt_mk_eq_component (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (a : Additive ↑zHat.toProfinite.toTop) :
    (maximalProPQuotientEquivPadicInt ℓ) ((maximalProPQuotient.mk ℓ ↑zHat.toProfinite.toTop) (Additive.toMul a)) = Multiplicative.ofAdd ((component ℓ) a)

    Agreement with the maximal pro-ℓ quotient. Tau Ceti's identification of the maximal pro-ℓ quotient of zHat with ℤ_[ℓ] sends the class of a profinite integer to its ℓ-adic component.

    source
    theorem TauCeti.zHat.component_surjective (ℓ : ℕ) [Fact (Nat.Prime ℓ)] :
    Function.Surjective ⇑(component ℓ)

    The ℓ-adic component is surjective: it is the identification of the maximal pro-ℓ quotient of zHat with ℤ_[ℓ], after the quotient map.