Continuity of the reduction of X → R modulo one vector with a unit coordinate

Over a topological ring R, the reduction

LinearMap.piSplitAtQuot x₀ w hw q : (X → R) →ₗ[R] ({x // x ≠ x₀} → R) × R ⧸ (q)

of TauCeti.LinearAlgebra.Quotient.PiSpanSingleton, which sends u to the coordinates u x - u x₀ * w x for x ≠ x₀ together with the class of u x₀ modulo q, is continuous for the product topology on X → R and the quotient topology on R ⧸ (q). Since the coordinate formula involves only subtraction and multiplication by the constants w x, continuity of these two operations on R suffices.

The reduction is also packaged as a continuous homomorphism between the multiplicative type tags of the two additive groups, which is the form in which it is applied to abelian pro-p groups written multiplicatively.

Main definitions

• TauCeti.ContinuousMonoidHom.piSplitAtQuotMultiplicative: the reduction as a continuous homomorphism Multiplicative (X → R) →ₜ* Multiplicative (({x // x ≠ x₀} → R) × R ⧸ (q)).

Main results

• TauCeti.LinearMap.continuous_piSplitAtQuot: the reduction is continuous.
• TauCeti.ContinuousMonoidHom.piSplitAtQuotMultiplicative_ofAdd: the value of the multiplicative form on ofAdd u is ofAdd of the reduction of u.

theorem TauCeti.LinearMap.continuous_piSplitAtQuot {R : Type u_1} [Ring R] [TopologicalSpace R] [ContinuousSub R] [ContinuousMul R] {X : Type u_2} (x₀ : X) (w : X → R) (hw : w x₀ = 1) (q : R) : Continuous ⇑(piSplitAtQuot x₀ w hw q)

The reduction (X → R) → ({x // x ≠ x₀} → R) × R ⧸ (q) of TauCeti.LinearMap.piSplitAtQuot is continuous, for the product topology on X → R and the quotient topology on R ⧸ (q).

noncomputable def TauCeti.ContinuousMonoidHom.piSplitAtQuotMultiplicative {R : Type u_1} [Ring R] [TopologicalSpace R] [ContinuousSub R] [ContinuousMul R] {X : Type u_2} (x₀ : X) (w : X → R) (hw : w x₀ = 1) (q : R) : Multiplicative (X → R) →ₜ* Multiplicative (({ x : X // x ≠ x₀ } → R) × R ⧸ Ideal.span {q})

The reduction TauCeti.LinearMap.piSplitAtQuot as a continuous homomorphism Multiplicative (X → R) →ₜ* Multiplicative (({x // x ≠ x₀} → R) × R ⧸ (q)) between the multiplicative type tags.

Equations

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

@[simp]

theorem TauCeti.ContinuousMonoidHom.piSplitAtQuotMultiplicative_ofAdd {R : Type u_1} [Ring R] [TopologicalSpace R] [ContinuousSub R] [ContinuousMul R] {X : Type u_2} (x₀ : X) (w : X → R) (hw : w x₀ = 1) (q : R) (u : X → R) : (piSplitAtQuotMultiplicative x₀ w hw q) (Multiplicative.ofAdd u) = Multiplicative.ofAdd ((LinearMap.piSplitAtQuot x₀ w hw q) u)