Jet groups of formal coordinates

For N : ℕ, two formal coordinates over a commutative ring R have the same N-jet when they agree modulo X ^ (N + 1), that is, when their coefficients agree through degree N. This congruence is compatible with composition on both sides: f (a) ≡ f (b) whenever a ≡ b, and f (a) ≡ g (a) whenever f ≡ g, modulo X ^ (N + 1). Hence the coordinates congruent to the identity X form a normal subgroup jetKernel R N, and the quotient is the group Jet R N of N-jets, with multiplication given by truncated composition. For N ≤ M truncation is a surjective homomorphism Jet R M →* Jet R N.

The full coordinate group is the inverse limit of its jet groups: a compatible family of jets comes from a unique formal coordinate, whose degree-n coefficient is read off from the n-jet. Giving each jet group the discrete topology and the coordinate group the topology induced by all of its jets, two coordinates are close when they agree modulo a high power of X. The comparison with the closed subgroup of compatible families in the product of the jet groups is then an isomorphism of topological groups.

Main definitions

• TauCeti.FormalCoordinate.jetKernel R N: the coordinates congruent to X modulo X ^ (N + 1).
• TauCeti.FormalCoordinate.Jet R N: the group of N-jets of formal coordinates.
• TauCeti.FormalCoordinate.jet N: the N-jet of a coordinate, as a homomorphism.
• TauCeti.FormalCoordinate.Jet.truncate: truncation Jet R M →* Jet R N for N ≤ M.
• TauCeti.FormalCoordinate.Jet.map f N: base change of N-jets along f : R →+* S.
• TauCeti.FormalCoordinate.jetLimit R: the compatible families of jets, a closed subgroup of the product of the jet groups.
• TauCeti.FormalCoordinate.jetLimitEquiv R: the isomorphism of topological groups between the formal coordinates and the compatible families of jets.

Main results

• TauCeti.FormalCoordinate.jet_eq_jet_iff: two coordinates have the same N-jet if and only if they agree modulo X ^ (N + 1).
• TauCeti.FormalCoordinate.tendsto_iff_X_pow_dvd: convergence of coordinates is eventual agreement modulo each power of X.
• TauCeti.FormalCoordinate.isClosed_jetLimit: the compatible families form a closed subgroup.
• TauCeti.FormalCoordinate.Jet.map_jet, TauCeti.FormalCoordinate.Jet.truncate_map: passing to jets and truncating jets are natural in the coefficients.
• TauCeti.FormalCoordinate.continuous_map: base change of formal coordinates is continuous.

theorem TauCeti.FormalCoordinate.X_pow_dvd_mul_sub_mul_left {R : Type u_1} [CommRing R] {n : ℕ} (χ : FormalCoordinate R) {φ ψ : FormalCoordinate R} (h : PowerSeries.X ^ n ∣ φ.toPowerSeries - ψ.toPowerSeries) : PowerSeries.X ^ n ∣ (χ * φ).toPowerSeries - (χ * ψ).toPowerSeries

Composing on the left with a fixed coordinate preserves congruence modulo X ^ n.

theorem TauCeti.FormalCoordinate.X_pow_dvd_mul_sub_mul_right {R : Type u_1} [CommRing R] {n : ℕ} (χ : FormalCoordinate R) {φ ψ : FormalCoordinate R} (h : PowerSeries.X ^ n ∣ φ.toPowerSeries - ψ.toPowerSeries) : PowerSeries.X ^ n ∣ (φ * χ).toPowerSeries - (ψ * χ).toPowerSeries

Composing on the right with a fixed coordinate preserves congruence modulo X ^ n.

def TauCeti.FormalCoordinate.jetKernel (R : Type u_1) [CommRing R] (N : ℕ) : Subgroup (FormalCoordinate R)

The coordinates congruent to the identity X modulo X ^ (N + 1): the kernel of passing to N-jets.

theorem TauCeti.FormalCoordinate.mem_jetKernel {R : Type u_1} [CommRing R] {N : ℕ} {φ : FormalCoordinate R} : φ ∈ jetKernel R N ↔ PowerSeries.X ^ (N + 1) ∣ φ.toPowerSeries - PowerSeries.X

theorem TauCeti.FormalCoordinate.jetKernel_mono {R : Type u_1} [CommRing R] {N M : ℕ} (h : N ≤ M) : jetKernel R M ≤ jetKernel R N

Agreement with X modulo a higher power of X implies agreement modulo a lower one.

instance TauCeti.FormalCoordinate.instNormalJetKernel {R : Type u_1} [CommRing R] (N : ℕ) : (jetKernel R N).Normal

def TauCeti.FormalCoordinate.Jet (R : Type u_1) [CommRing R] (N : ℕ) : Type u_1

The group of N-jets of formal coordinates: formal coordinates modulo X ^ (N + 1), with multiplication given by truncated composition.

@[instance_reducible]

noncomputable instance TauCeti.FormalCoordinate.Jet.instGroup {R : Type u_1} [CommRing R] (N : ℕ) : Group (Jet R N)

@[instance_reducible]

instance TauCeti.FormalCoordinate.Jet.instTopologicalSpace {R : Type u_1} [CommRing R] (N : ℕ) : TopologicalSpace (Jet R N)

Jet groups carry the discrete topology.

instance TauCeti.FormalCoordinate.Jet.instDiscreteTopology {R : Type u_1} [CommRing R] (N : ℕ) : DiscreteTopology (Jet R N)

noncomputable def TauCeti.FormalCoordinate.jet {R : Type u_1} [CommRing R] (N : ℕ) : FormalCoordinate R →* Jet R N

The N-jet of a formal coordinate: its class modulo X ^ (N + 1).

theorem TauCeti.FormalCoordinate.jet_surjective {R : Type u_1} [CommRing R] (N : ℕ) : Function.Surjective ⇑(jet N)

@[simp]

theorem TauCeti.FormalCoordinate.ker_jet {R : Type u_1} [CommRing R] (N : ℕ) : (jet N).ker = jetKernel R N

theorem TauCeti.FormalCoordinate.jet_eq_jet_iff {R : Type u_1} [CommRing R] {N : ℕ} {φ ψ : FormalCoordinate R} : (jet N) φ = (jet N) ψ ↔ PowerSeries.X ^ (N + 1) ∣ φ.toPowerSeries - ψ.toPowerSeries

Two formal coordinates have the same N-jet exactly when they agree modulo X ^ (N + 1).

theorem TauCeti.FormalCoordinate.jet_eq_jet_iff_coeff {R : Type u_1} [CommRing R] {N : ℕ} {φ ψ : FormalCoordinate R} : (jet N) φ = (jet N) ψ ↔ ∀ m ≤ N, (PowerSeries.coeff m) φ.toPowerSeries = (PowerSeries.coeff m) ψ.toPowerSeries

Two formal coordinates have the same N-jet exactly when their coefficients agree through degree N.

theorem TauCeti.FormalCoordinate.jet_eq_one_iff {R : Type u_1} [CommRing R] {N : ℕ} {φ : FormalCoordinate R} : (jet N) φ = 1 ↔ PowerSeries.X ^ (N + 1) ∣ φ.toPowerSeries - PowerSeries.X

A formal coordinate has trivial N-jet exactly when it agrees with X modulo X ^ (N + 1).

noncomputable def TauCeti.FormalCoordinate.Jet.truncate {R : Type u_1} [CommRing R] {N M : ℕ} (h : N ≤ M) : Jet R M →* Jet R N

For N ≤ M, the truncation of M-jets to N-jets.

@[simp]

theorem TauCeti.FormalCoordinate.Jet.truncate_jet {R : Type u_1} [CommRing R] {N M : ℕ} (h : N ≤ M) (φ : FormalCoordinate R) : (truncate h) ((jet M) φ) = (jet N) φ

theorem TauCeti.FormalCoordinate.Jet.truncate_comp_jet {R : Type u_1} [CommRing R] {N M : ℕ} (h : N ≤ M) : (truncate h).comp (jet M) = jet N

theorem TauCeti.FormalCoordinate.Jet.truncate_surjective {R : Type u_1} [CommRing R] {N M : ℕ} (h : N ≤ M) : Function.Surjective ⇑(truncate h)

@[simp]

theorem TauCeti.FormalCoordinate.Jet.truncate_refl {R : Type u_1} [CommRing R] {N : ℕ} (x : Jet R N) : (truncate ⋯) x = x

@[simp]

theorem TauCeti.FormalCoordinate.Jet.truncate_truncate {R : Type u_1} [CommRing R] {N M L : ℕ} (h₁ : N ≤ M) (h₂ : M ≤ L) (x : Jet R L) : (truncate h₁) ((truncate h₂) x) = (truncate ⋯) x

Base change of jets

theorem TauCeti.FormalCoordinate.jetKernel_le_comap_map {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (N : ℕ) : jetKernel R N ≤ Subgroup.comap (map f) (jetKernel S N)

Base change of coefficients preserves agreement with X modulo X ^ (N + 1).

noncomputable def TauCeti.FormalCoordinate.Jet.map {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (N : ℕ) : Jet R N →* Jet S N

Base change of N-jets along a ring homomorphism f : R →+* S, induced by base change of formal coordinates.

@[simp]

theorem TauCeti.FormalCoordinate.Jet.map_jet {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (N : ℕ) (φ : FormalCoordinate R) : (map f N) ((jet N) φ) = (jet N) ((FormalCoordinate.map f) φ)

theorem TauCeti.FormalCoordinate.Jet.map_comp_jet {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (N : ℕ) : (map f N).comp (jet N) = (jet N).comp (FormalCoordinate.map f)

@[simp]

theorem TauCeti.FormalCoordinate.Jet.truncate_map {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) {N M : ℕ} (h : N ≤ M) (x : Jet R M) : (truncate h) ((map f M) x) = (map f N) ((truncate h) x)

Jet truncation is natural in the coefficients.

theorem TauCeti.FormalCoordinate.Jet.truncate_comp_map {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) {N M : ℕ} (h : N ≤ M) : (truncate h).comp (map f M) = (map f N).comp (truncate h)

@[simp]

theorem TauCeti.FormalCoordinate.Jet.map_id {R : Type u_1} [CommRing R] (N : ℕ) : map (RingHom.id R) N = MonoidHom.id (Jet R N)

@[simp]

theorem TauCeti.FormalCoordinate.Jet.map_map {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) {T : Type u_3} [CommRing T] (g : S →+* T) (N : ℕ) (x : Jet R N) : (map g N) ((map f N) x) = (map (g.comp f) N) x

theorem TauCeti.FormalCoordinate.Jet.map_injective {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {f : R →+* S} (hf : Function.Injective ⇑f) (N : ℕ) : Function.Injective ⇑(map f N)

Base change of jets along an injective ring homomorphism is injective.

The inverse limit of the jet groups

noncomputable def TauCeti.FormalCoordinate.jetLimit (R : Type u_1) [CommRing R] : Subgroup ((N : ℕ) → Jet R N)

The compatible families of jets: the inverse limit of the jet groups along truncation, as a subgroup of their product.

theorem TauCeti.FormalCoordinate.mem_jetLimit {R : Type u_1} [CommRing R] {x : (N : ℕ) → Jet R N} : x ∈ jetLimit R ↔ ∀ ⦃N M : ℕ⦄ (h : N ≤ M), (Jet.truncate h) (x M) = x N

noncomputable def TauCeti.FormalCoordinate.jets (R : Type u_1) [CommRing R] : FormalCoordinate R →* (N : ℕ) → Jet R N

The family of all jets of a formal coordinate.

@[simp]

theorem TauCeti.FormalCoordinate.jets_apply {R : Type u_1} [CommRing R] (φ : FormalCoordinate R) (N : ℕ) : (jets R) φ N = (jet N) φ

theorem TauCeti.FormalCoordinate.jets_injective {R : Type u_1} [CommRing R] : Function.Injective ⇑(jets R)

A formal coordinate is determined by its jets.

theorem TauCeti.FormalCoordinate.range_jets {R : Type u_1} [CommRing R] : (jets R).range = jetLimit R

Every compatible family of jets is the family of jets of a formal coordinate.

The topology of agreement modulo powers of X

@[instance_reducible]

noncomputable instance TauCeti.FormalCoordinate.instTopologicalSpace {R : Type u_1} [CommRing R] : TopologicalSpace (FormalCoordinate R)

Formal coordinates carry the topology induced by all of their jets, each jet group being discrete: coordinates are close when they agree modulo a high power of X.

theorem TauCeti.FormalCoordinate.isInducing_jets {R : Type u_1} [CommRing R] : Topology.IsInducing ⇑(jets R)

theorem TauCeti.FormalCoordinate.isEmbedding_jets {R : Type u_1} [CommRing R] : Topology.IsEmbedding ⇑(jets R)

instance TauCeti.FormalCoordinate.instIsTopologicalGroup {R : Type u_1} [CommRing R] : IsTopologicalGroup (FormalCoordinate R)

instance TauCeti.FormalCoordinate.instT2Space {R : Type u_1} [CommRing R] : T2Space (FormalCoordinate R)

theorem TauCeti.FormalCoordinate.continuous_jet {R : Type u_1} [CommRing R] (N : ℕ) : Continuous ⇑(jet N)

theorem TauCeti.FormalCoordinate.continuous_map {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) : Continuous ⇑(map f)

Base change of formal coordinates is continuous for the topologies of agreement modulo powers of X.

theorem TauCeti.FormalCoordinate.isOpen_jetKernel {R : Type u_1} [CommRing R] (N : ℕ) : IsOpen ↑(jetKernel R N)

The coordinates congruent to X modulo X ^ (N + 1) form an open subgroup.

theorem TauCeti.FormalCoordinate.tendsto_iff_X_pow_dvd {R : Type u_1} [CommRing R] {ι : Type u_2} {l : Filter ι} (f : ι → FormalCoordinate R) (φ : FormalCoordinate R) : Filter.Tendsto f l (nhds φ) ↔ ∀ (N : ℕ), ∀ᶠ (i : ι) in l, PowerSeries.X ^ (N + 1) ∣ (f i).toPowerSeries - φ.toPowerSeries

A family of formal coordinates converges exactly when it eventually agrees with the limit modulo each power of X.

theorem TauCeti.FormalCoordinate.hasBasis_nhds {R : Type u_1} [CommRing R] (φ : FormalCoordinate R) : (nhds φ).HasBasis (fun (x : ℕ) => True) fun (N : ℕ) => {ψ : FormalCoordinate R | PowerSeries.X ^ (N + 1) ∣ ψ.toPowerSeries - φ.toPowerSeries}

The congruence classes modulo powers of X form a neighbourhood basis.

theorem TauCeti.FormalCoordinate.isClosed_jetLimit {R : Type u_1} [CommRing R] : IsClosed ↑(jetLimit R)

The compatible families of jets form a closed subgroup of the product of the jet groups.

noncomputable def TauCeti.FormalCoordinate.jetLimitEquiv (R : Type u_1) [CommRing R] : FormalCoordinate R ≃ₜ* ↥(jetLimit R)

The formal coordinates are the inverse limit of their jet groups: passing to all jets is an isomorphism of topological groups onto the compatible families of jets.

@[simp]

theorem TauCeti.FormalCoordinate.jetLimitEquiv_apply_coe {R : Type u_1} [CommRing R] (φ : FormalCoordinate R) (N : ℕ) : ↑((jetLimitEquiv R) φ) N = (jet N) φ

@[simp]

theorem TauCeti.FormalCoordinate.jets_jetLimitEquiv_symm_apply {R : Type u_1} [CommRing R] (x : ↥(jetLimit R)) : (jets R) ((jetLimitEquiv R).symm x) = ↑x