Divided powers on ℤ_[p]

Given a divided power algebra (B, J, δ) and an injective ring morphism f : A →+* B, if I is an A-ideal such that I.map f = J and such that for all n : ℕ, x ∈ I, the preimage of hJ.dpow n (f x) under f belongs to I, we get an induced divided power structure on I.

We specialize this construction to the coercion map ℤ_[p] →+* ℚ_[p] to get a divided power structure on the ideal (p) ⊆ ℤ_[p]. This divided power structure is given by the family of maps fun n x ↦ x^n / n!.

TODO: If K is a p-adic local field with ring of integers R and uniformizer π such that p = u * π^e for some unit u, then the ideal (π) ⊆ R has divided powers if and only if e ≤ p - 1.

noncomputable def PadicInt.dividedPowers_of_injective {A : Type u_1} {B : Type u_2} [CommSemiring A] [CommSemiring B] (I : Ideal A) (J : Ideal B) (f : A →+* B) (hf : Function.Injective ⇑f) (hJ : DividedPowers J) (hIJ : Ideal.map f I = J) (hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ (y : A) (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)) : DividedPowers I

Given a divided power algebra (B, J, δ) and an injective ring morphism f : A →+* B, if I is an A-ideal such that I.map f = J and such that for all n : ℕ, x ∈ I, the preimage of hJ.dpow n (f x) under f belongs to I, this is the induced divided power structure on I.

Equations

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

noncomputable def PadicInt.dividedPowers (p : ℕ) [hp : Fact (Nat.Prime p)] : DividedPowers (Ideal.span {↑p})

The family ℕ → Ideal.span {(p : ℤ_[p])} → ℤ_[p] given by dpow n x = x ^ n / n! is a divided power structure on the ℤ_[p]-ideal (p).

Equations

• PadicInt.dividedPowers p = PadicInt.dividedPowers_of_injective (Ideal.span {↑p}) ⊤ PadicInt.Coe.ringHom ⋯ (DividedPowers.RatAlgebra.dividedPowers ⊤) ⋯ ⋯

theorem PadicInt.coe_dpow_eq (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) (x : ℤ_[p]) : ↑((dividedPowers p).dpow n x) = if x_1 : x ∈ Ideal.span {↑p} then Ring.inverse ↑n.factorial * ↑x ^ n else 0