Renaming the variables of A⟨X⟩_T

An embedding e : Fin k ↪ Fin m of variables renames power series in k variables to power series in m variables, Xᵢ ↦ X_{e i}. Renaming preserves weighted restrictedness as soon as each weight T i lies in the weight S (e i) of the variable it is sent to, and so induces a continuous ring homomorphism A⟨X⟩_T → A⟨X⟩_S.

At the trivial weight these include the two maps A⟨ζ⟩ → A⟨X, Y⟩, ζ ↦ X and ζ ↦ Y, that compare the pieces of a two-piece Laurent cover with their overlap in Wedhorn's Lemma 8.33.

Main definitions

• TauCeti.Huber.weightedRename: the ring homomorphism A⟨X⟩_T → A⟨X⟩_S induced by an embedding of the variables; TauCeti.Huber.weightedRenameAlgHom is its A-algebra-homomorphism form, and TauCeti.Huber.coe_weightedRename says it is MvPowerSeries.rename.

Main results

• TauCeti.Huber.IsWeightedRestricted.rename: renaming along an embedding carries T-restricted series to S-restricted ones.
• TauCeti.Huber.weightedRename_weightedC and TauCeti.Huber.weightedRename_weightedX: the induced homomorphism fixes the constants and sends Xᵢ to X_{e i}.
• TauCeti.Huber.continuous_weightedRename: it is continuous.
• TauCeti.Huber.weightedRename_injective and TauCeti.Huber.weightedRename_inj (simp): it is injective, so equality may be read off after renaming.
• TauCeti.Huber.weightedRename_id and TauCeti.Huber.weightedRename_comp: the identity and composition laws, which make the construction functorial in the variables.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Remark and Definition 5.48, and the proof of Lemma 8.33.

Provenance

The renaming is Mathlib's MvPowerSeries.rename. AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit 37bbdaeb9, projects/AdicSpaces/Adic spaces/TateAlgebra.lean, has the two trivial-weight maps from its TateAlgebra A into TateAlgebra₂ A as posIncl and negIncl, built on its own varInclHom, with posIncl_algebraMap and posIncl_X and their negIncl counterparts. Those are the two trivial-weight instances of weightedRename here, which is defined for an arbitrary embedding of the variables and arbitrary weights T i ⊆ S (e i).

theorem TauCeti.Huber.IsWeightedRestricted.rename {A : Type u_1} [CommRing A] [TopologicalSpace A] {k m : ℕ} (e : Fin k ↪ Fin m) {T : Fin k → Set A} {S : Fin m → Set A} (hTS : ∀ (i : Fin k), T i ⊆ S (e i)) {f : MvPowerSeries (Fin k) A} (hf : IsWeightedRestricted T f) : IsWeightedRestricted S ((MvPowerSeries.rename ⇑e) f)

Renaming preserves weighted restrictedness: along an embedding e of the variables with each T i ⊆ S (e i), a T-restricted series renames to an S-restricted one. The weights of the variables outside the image of e are arbitrary. This renames the variables, where TauCeti.Huber.IsWeightedRestricted.map changes the coefficient ring.

noncomputable def TauCeti.Huber.weightedRename {A : Type u_1} [CommRing A] [TopologicalSpace A] {k m : ℕ} [NonarchimedeanRing A] (e : Fin k ↪ Fin m) {T : Fin k → Set A} {S : Fin m → Set A} (hT : IsWeightFamily T) (hS : IsWeightFamily S) (hTS : ∀ (i : Fin k), T i ⊆ S (e i)) : ↥(weightedRestrictedSubring T hT) →+* ↥(weightedRestrictedSubring S hS)

The homomorphism A⟨X⟩_T → A⟨X⟩_S induced by an embedding e of the variables, sending Xᵢ to X_{e i}. Each weight T i must lie in the weight S (e i) of its image.

It moves the variables and keeps the coefficients, where TauCeti.Huber.weightedMap moves the coefficients along a ring map and keeps the variables. Its values are computed by TauCeti.Huber.coe_weightedRename.

Equations

• TauCeti.Huber.weightedRename e hT hS hTS = (MvPowerSeries.rename ⇑e).restrict (TauCeti.Huber.weightedRestrictedSubring T hT) (TauCeti.Huber.weightedRestrictedSubring S hS) ⋯

@[simp]

theorem TauCeti.Huber.coe_weightedRename {A : Type u_1} [CommRing A] [TopologicalSpace A] {k m : ℕ} [NonarchimedeanRing A] (e : Fin k ↪ Fin m) {T : Fin k → Set A} {S : Fin m → Set A} {hT : IsWeightFamily T} {hS : IsWeightFamily S} (hTS : ∀ (i : Fin k), T i ⊆ S (e i)) (f : ↥(weightedRestrictedSubring T hT)) : ↑((weightedRename e hT hS hTS) f) = (MvPowerSeries.rename ⇑e) ↑f

weightedRename is MvPowerSeries.rename with its domain and codomain cut down.

@[simp]

theorem TauCeti.Huber.weightedRename_weightedC {A : Type u_1} [CommRing A] [TopologicalSpace A] {k m : ℕ} [NonarchimedeanRing A] (e : Fin k ↪ Fin m) {T : Fin k → Set A} {S : Fin m → Set A} {hT : IsWeightFamily T} {hS : IsWeightFamily S} (hTS : ∀ (i : Fin k), T i ⊆ S (e i)) (a : A) : (weightedRename e hT hS hTS) ((weightedC T hT) a) = (weightedC S hS) a

weightedRename fixes the constant series.

noncomputable def TauCeti.Huber.weightedRenameAlgHom {A : Type u_1} [CommRing A] [TopologicalSpace A] {k m : ℕ} [NonarchimedeanRing A] (e : Fin k ↪ Fin m) {T : Fin k → Set A} {S : Fin m → Set A} (hT : IsWeightFamily T) (hS : IsWeightFamily S) (hTS : ∀ (i : Fin k), T i ⊆ S (e i)) : ↥(weightedRestrictedSubring T hT) →ₐ[A] ↥(weightedRestrictedSubring S hS)

The A-algebra-homomorphism form of weightedRename.

Equations

• TauCeti.Huber.weightedRenameAlgHom e hT hS hTS = { toRingHom := TauCeti.Huber.weightedRename e hT hS hTS, commutes' := ⋯ }

@[simp]

theorem TauCeti.Huber.weightedRenameAlgHom_apply {A : Type u_1} [CommRing A] [TopologicalSpace A] {k m : ℕ} [NonarchimedeanRing A] (e : Fin k ↪ Fin m) {T : Fin k → Set A} {S : Fin m → Set A} (hT : IsWeightFamily T) (hS : IsWeightFamily S) (hTS : ∀ (i : Fin k), T i ⊆ S (e i)) (f : ↥(weightedRestrictedSubring T hT)) : (weightedRenameAlgHom e hT hS hTS) f = (weightedRename e hT hS hTS) f

The algebra-homomorphism form has the same underlying function as weightedRename.

@[simp]

theorem TauCeti.Huber.weightedRename_weightedX {A : Type u_1} [CommRing A] [TopologicalSpace A] {k m : ℕ} [NonarchimedeanRing A] (e : Fin k ↪ Fin m) {T : Fin k → Set A} {S : Fin m → Set A} {hT : IsWeightFamily T} {hS : IsWeightFamily S} (hTS : ∀ (i : Fin k), T i ⊆ S (e i)) (i : Fin k) : (weightedRename e hT hS hTS) (weightedX T hT i) = weightedX S hS (e i)

weightedRename sends the variable Xᵢ to X_{e i}.

theorem TauCeti.Huber.continuous_weightedRename {A : Type u_1} [CommRing A] [TopologicalSpace A] {k m : ℕ} [NonarchimedeanRing A] (e : Fin k ↪ Fin m) {T : Fin k → Set A} {S : Fin m → Set A} (hT : IsWeightFamily T) (hS : IsWeightFamily S) (hTS : ∀ (i : Fin k), T i ⊆ S (e i)) : Continuous ⇑(weightedRename e hT hS hTS)

weightedRename is continuous for the weighted topologies, so it is a morphism of topological rings.

theorem TauCeti.Huber.weightedRename_injective {A : Type u_1} [CommRing A] [TopologicalSpace A] {k m : ℕ} [NonarchimedeanRing A] (e : Fin k ↪ Fin m) {T : Fin k → Set A} {S : Fin m → Set A} {hT : IsWeightFamily T} {hS : IsWeightFamily S} (hTS : ∀ (i : Fin k), T i ⊆ S (e i)) : Function.Injective ⇑(weightedRename e hT hS hTS)

weightedRename is injective, because MvPowerSeries.rename along an embedding is and the coercion to the ambient series ring is.

@[simp]

theorem TauCeti.Huber.weightedRename_inj {A : Type u_1} [CommRing A] [TopologicalSpace A] {k m : ℕ} [NonarchimedeanRing A] (e : Fin k ↪ Fin m) {T : Fin k → Set A} {S : Fin m → Set A} {hT : IsWeightFamily T} {hS : IsWeightFamily S} (hTS : ∀ (i : Fin k), T i ⊆ S (e i)) (f g : ↥(weightedRestrictedSubring T hT)) : (weightedRename e hT hS hTS) f = (weightedRename e hT hS hTS) g ↔ f = g

Equality after renaming is equality: the iff form of TauCeti.Huber.weightedRename_injective.

@[simp]

theorem TauCeti.Huber.weightedRename_id {A : Type u_1} [CommRing A] [TopologicalSpace A] {k : ℕ} [NonarchimedeanRing A] {T : Fin k → Set A} (hT : IsWeightFamily T) : weightedRename (Function.Embedding.refl (Fin k)) hT hT ⋯ = RingHom.id ↥(weightedRestrictedSubring T hT)

The identity law: renaming along Function.Embedding.refl is the identity.

theorem TauCeti.Huber.weightedRename_comp {A : Type u_1} [CommRing A] [TopologicalSpace A] {k m : ℕ} [NonarchimedeanRing A] {n : ℕ} (e₁ : Fin k ↪ Fin m) (e₂ : Fin m ↪ Fin n) {T : Fin k → Set A} {S : Fin m → Set A} {R : Fin n → Set A} (hT : IsWeightFamily T) (hS : IsWeightFamily S) (hR : IsWeightFamily R) (hTS : ∀ (i : Fin k), T i ⊆ S (e₁ i)) (hSR : ∀ (i : Fin m), S i ⊆ R (e₂ i)) : weightedRename (e₁.trans e₂) hT hR ⋯ = (weightedRename e₂ hS hR hSR).comp (weightedRename e₁ hT hS hTS)

The composition law: renaming along a composite embedding is the composite of the renamings. With weightedRename_id this is what makes A⟨X⟩_T functorial in the variables, as weightedMap_comp and weightedMap_id do for the coefficient ring.