How to present the ring of power series as a limit in Ring?

Stream: mathlib4

[Jiatong Yang]

I'd like to present the ring k[[x]] as the categorical limit of k[x]/(x^n), but I meet trouble defining the cone.
It's too difficult for me to show the commutativity of k[[x]] -> k[x]/(x^n) -> k[x]/(x^m). And maybe there is a better way to give the map k[[x]] -> k[x]/(x^n)? (I'm now using PowerSeries.aeval, but it seems hard)
I need help.

import Mathlib
open CategoryTheory Polynomial CategoryTheory.Limits

universe u

/- Consider F : Nat^op -> Ring with F(n) = k[x]/(x^n)
The limit of this diagram is the ring of power series in x with coefficients in k.
-/
variable (k : Type u) [Field k]

noncomputable def F : Natᵒᵖ ⥤ RingCat :=
  {
    obj := fun ⟨n⟩ => RingCat.of ((k[X] ⧸ Ideal.span {(X ^ n : k[X])}))
    map := fun {A B} f => match A, B with
      | ⟨n⟩, ⟨m⟩ => match f with
        | ⟨⟨⟨(f : m ≤ n)⟩⟩⟩ =>
          RingCat.ofHom (Ideal.Quotient.factor (Ideal.span_singleton_le_span_singleton.mpr (pow_dvd_pow X f)))
  }

noncomputable def cone_F : Cone (F k) :=
  {
    pt := RingCat.of (PowerSeries k)
    π := {
      app := by
        rintro ⟨n⟩
        simp [F]
        let disc_top_inst₁ : UniformSpace k := ⊥
        let disc_top_inst₂ : UniformSpace (k[X] ⧸ Ideal.span {(X ^ n : k[X])}) := ⊥
        let disc_top_inst₃ : ContinuousSMul k (k[X] ⧸ Ideal.span {(X ^ n : k[X])}) := ⟨by continuity⟩
        let has_eval : PowerSeries.HasEval ((Ideal.Quotient.mk (Ideal.span {(X ^ n : k[X])})) X) := by
          simp [PowerSeries.HasEval]
          refine IsNilpotent.isTopologicallyNilpotent ⟨n, ?_⟩
          rw [← map_pow]
          simp
        exact RingCat.ofHom (AlgHom.toRingHom (PowerSeries.aeval (R := k) (S := k[X] ⧸ Ideal.span {(X ^ n : k[X])}) (a := Ideal.Quotient.mk _ X) has_eval))

      naturality := by
        rintro ⟨n⟩ ⟨m⟩ ⟨⟨⟨(f : m ≤ n)⟩⟩⟩
        simp
        ext (x : PowerSeries k)
        simp [F, PowerSeries.aeval_eq_sum]
        have eq_zero (s : ℕ) : ∀ d ∉ Finset.range s, (PowerSeries.coeff d) x • (Ideal.Quotient.mk (Ideal.span {(X ^ s : k[X])})) X ^ d = 0 := by sorry
        let disc_top_inst {s : ℕ} : UniformSpace (k[X] ⧸ Ideal.span {(X ^ s : k[X])}) := ⊥
        rw [tsum_eq_sum (eq_zero n), tsum_eq_sum (eq_zero m)]
        sorry

    }
  }

[Notification Bot]

This topic was moved here from #lean4 > How to present the ring of power series as a limit in Ring? by Johan Commelin.

[Johan Commelin]

@Jiatong Yang Hi! I've moved your message to a different channel