The quotient of X → R by one vector with a unit coordinate

Let R be a ring, X a type with a distinguished point x₀, and w : X → R a vector with w x₀ = 1. Every u : X → R decomposes uniquely as u x₀ • w plus a vector vanishing at x₀, which gives a change of coordinates on the product module X → R: the new coordinates of u are u x - u x₀ * w x for x ≠ x₀ together with u x₀. (For finite X this is the change of basis replacing the coordinate vector at x₀ by w.) The resulting linear isomorphism

LinearEquiv.piSplitAt x₀ w hw : (X → R) ≃ₗ[R] ({x // x ≠ x₀} → R) × R

sends c • w to (0, c). Composing with reduction modulo an element q in the second factor gives a surjective linear map onto ({x // x ≠ x₀} → R) × R ⧸ (q) whose kernel is exactly the span of the single vector q • w, hence the identification

(X → R) ⧸ span {q • w} ≃ₗ[R] ({x // x ≠ x₀} → R) × R ⧸ (q).

Every vector v with a coordinate v x₀ dividing all the other coordinates has the shape v = v x₀ • w with w x₀ = 1 (exists_eq_smul_of_forall_dvd); over a valuation ring every vector on a finite nonempty index type has such a coordinate. This is the linear algebra behind the structure of the abelianization of a one-relator pro-p group: the relator contributes the single vector v = q • w to ℤ_p^n, and the quotient is ℤ_p^{n-1} × ℤ_p/q.

Main definitions

• TauCeti.LinearEquiv.piSplitAt: the change of coordinates (X → R) ≃ₗ[R] ({x // x ≠ x₀} → R) × R replacing the coordinate at x₀ by the coordinate along w.
• TauCeti.LinearMap.piSplitAtQuot: the composite with reduction modulo q in the second factor.
• TauCeti.LinearEquiv.piQuotSpanSmul: the induced isomorphism (X → R) ⧸ span {q • w} ≃ₗ[R] ({x // x ≠ x₀} → R) × R ⧸ (q).

Main results

• TauCeti.LinearMap.ker_piSplitAtQuot, TauCeti.LinearMap.piSplitAtQuot_surjective: the kernel of the reduction is the span of q • w, and it is surjective.
• TauCeti.exists_eq_smul_of_forall_dvd: a vector with a coordinate dividing all the others is a multiple of a vector with a 1 at that coordinate.

theorem TauCeti.exists_eq_smul_of_forall_dvd {R : Type u_1} {X : Type u_2} [Monoid R] {v : X → R} {x₀ : X} (h : ∀ (x : X), v x₀ ∣ v x) : ∃ (w : X → R), w x₀ = 1 ∧ v = v x₀ • w

A vector with a coordinate v x₀ dividing every coordinate is v x₀ • w for a vector w with w x₀ = 1.

noncomputable def TauCeti.LinearEquiv.piSplitAt {R : Type u_1} [Ring R] {X : Type u_2} (x₀ : X) (w : X → R) (hw : w x₀ = 1) : (X → R) ≃ₗ[R] ({ x : X // x ≠ x₀ } → R) × R

The change of coordinates on X → R replacing the coordinate at x₀ by the coordinate along w. For w x₀ = 1, every u : X → R decomposes uniquely as u x₀ • w plus a vector vanishing at x₀; the new coordinates of u are u x - u x₀ * w x at x ≠ x₀ and u x₀ along w. For finite X this is the change of basis from the coordinate vectors to w together with the coordinate vectors at x ≠ x₀.

Equations

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

@[simp]

theorem TauCeti.LinearEquiv.piSplitAt_apply {R : Type u_1} [Ring R] {X : Type u_2} (x₀ : X) (w : X → R) (hw : w x₀ = 1) (u : X → R) : (piSplitAt x₀ w hw) u = (fun (x : { x : X // x ≠ x₀ }) => u ↑x - u x₀ * w ↑x, u x₀)

@[simp]

theorem TauCeti.LinearEquiv.piSplitAt_symm_apply {R : Type u_1} [Ring R] {X : Type u_2} (x₀ : X) (w : X → R) (hw : w x₀ = 1) [DecidableEq X] (a : ({ x : X // x ≠ x₀ } → R) × R) (x : X) : (piSplitAt x₀ w hw).symm a x = (if h : x = x₀ then 0 else a.1 ⟨x, h⟩) + a.2 * w x

theorem TauCeti.LinearEquiv.piSplitAt_smul {R : Type u_1} [Ring R] {X : Type u_2} (x₀ : X) (w : X → R) (hw : w x₀ = 1) (c : R) : (piSplitAt x₀ w hw) (c • w) = (0, c)

The change of coordinates sends a multiple of w to the corresponding multiple in the second factor.

theorem TauCeti.LinearEquiv.piSplitAt_single_of_ne {R : Type u_1} [Ring R] {X : Type u_2} (x₀ : X) (w : X → R) (hw : w x₀ = 1) [DecidableEq X] {x : X} (hx : x ≠ x₀) : (piSplitAt x₀ w hw) (Pi.single x 1) = (Pi.single ⟨x, hx⟩ 1, 0)

The change of coordinates fixes the coordinate vectors at x ≠ x₀.

theorem TauCeti.LinearEquiv.piSplitAt_single_self {R : Type u_1} [Ring R] {X : Type u_2} (x₀ : X) (w : X → R) (hw : w x₀ = 1) [DecidableEq X] : (piSplitAt x₀ w hw) (Pi.single x₀ 1) = (fun (x : { x : X // x ≠ x₀ }) => -w ↑x, 1)

The change of coordinates sends the coordinate vector at x₀ to (-w, 1): it is w minus the vector w - e_{x₀} supported away from x₀.

noncomputable def TauCeti.LinearMap.piSplitAtQuot {R : Type u_1} [Ring R] {X : Type u_2} (x₀ : X) (w : X → R) (hw : w x₀ = 1) (q : R) : (X → R) →ₗ[R] ({ x : X // x ≠ x₀ } → R) × R ⧸ Ideal.span {q}

The change of coordinates LinearEquiv.piSplitAt followed by reduction modulo q on the coordinate along w. Its kernel is the span of q • w (ker_piSplitAtQuot), and it is surjective (piSplitAtQuot_surjective).

Equations

• TauCeti.LinearMap.piSplitAtQuot x₀ w hw q = LinearMap.id.prodMap (Submodule.mkQ (Ideal.span {q})) ∘ₗ ↑(TauCeti.LinearEquiv.piSplitAt x₀ w hw)

@[simp]

theorem TauCeti.LinearMap.piSplitAtQuot_apply {R : Type u_1} [Ring R] {X : Type u_2} (x₀ : X) (w : X → R) (hw : w x₀ = 1) (q : R) (u : X → R) : (piSplitAtQuot x₀ w hw q) u = (fun (x : { x : X // x ≠ x₀ }) => u ↑x - u x₀ * w ↑x, Submodule.Quotient.mk (u x₀))

theorem TauCeti.LinearMap.piSplitAtQuot_piSplitAt_symm {R : Type u_1} [Ring R] {X : Type u_2} (x₀ : X) (w : X → R) (hw : w x₀ = 1) (q : R) (a : { x : X // x ≠ x₀ } → R) (b : R) : (piSplitAtQuot x₀ w hw q) ((LinearEquiv.piSplitAt x₀ w hw).symm (a, b)) = (a, Submodule.Quotient.mk b)

The reduction composed with the inverse change of coordinates is reduction modulo q on the second coordinate.

theorem TauCeti.LinearMap.piSplitAtQuot_surjective {R : Type u_1} [Ring R] {X : Type u_2} (x₀ : X) (w : X → R) (hw : w x₀ = 1) (q : R) : Function.Surjective ⇑(piSplitAtQuot x₀ w hw q)

The change of coordinates followed by reduction modulo q is surjective.

theorem TauCeti.LinearMap.piSplitAtQuot_single_of_ne {R : Type u_1} [Ring R] {X : Type u_2} (x₀ : X) (w : X → R) (hw : w x₀ = 1) (q : R) [DecidableEq X] {x : X} (hx : x ≠ x₀) : (piSplitAtQuot x₀ w hw q) (Pi.single x 1) = (Pi.single ⟨x, hx⟩ 1, 0)

The reduction fixes the coordinate vectors at x ≠ x₀.

theorem TauCeti.LinearMap.piSplitAtQuot_single_self {R : Type u_1} [Ring R] {X : Type u_2} (x₀ : X) (w : X → R) (hw : w x₀ = 1) (q : R) [DecidableEq X] : (piSplitAtQuot x₀ w hw q) (Pi.single x₀ 1) = (fun (x : { x : X // x ≠ x₀ }) => -w ↑x, Submodule.Quotient.mk 1)

The reduction sends the coordinate vector at x₀ to (-w, 1).

theorem TauCeti.LinearMap.ker_piSplitAtQuot {R : Type u_1} [Ring R] {X : Type u_2} (x₀ : X) (w : X → R) (hw : w x₀ = 1) (q : R) : (piSplitAtQuot x₀ w hw q).ker = R ∙ q • w

The kernel of the reduction is the span of q • w.

noncomputable def TauCeti.LinearEquiv.piQuotSpanSmul {R : Type u_1} [Ring R] {X : Type u_2} (x₀ : X) (w : X → R) (hw : w x₀ = 1) (q : R) : ((X → R) ⧸ R ∙ q • w) ≃ₗ[R] ({ x : X // x ≠ x₀ } → R) × R ⧸ Ideal.span {q}

The quotient of X → R by one vector. For w x₀ = 1, the quotient of X → R by the span of q • w is ({x // x ≠ x₀} → R) × R ⧸ (q), through the change of coordinates LinearEquiv.piSplitAt.

Equations

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

@[simp]

theorem TauCeti.LinearEquiv.piQuotSpanSmul_mk {R : Type u_1} [Ring R] {X : Type u_2} (x₀ : X) (w : X → R) (hw : w x₀ = 1) (q : R) (u : X → R) : (piQuotSpanSmul x₀ w hw q) (Submodule.Quotient.mk u) = (LinearMap.piSplitAtQuot x₀ w hw q) u

@[simp]

theorem TauCeti.LinearEquiv.piQuotSpanSmul_symm_mk {R : Type u_1} [Ring R] {X : Type u_2} (x₀ : X) (w : X → R) (hw : w x₀ = 1) (q : R) (a : { x : X // x ≠ x₀ } → R) (b : R) : (piQuotSpanSmul x₀ w hw q).symm (a, Submodule.Quotient.mk b) = Submodule.Quotient.mk ((piSplitAt x₀ w hw).symm (a, b))

The inverse of piQuotSpanSmul sends the class of (a, b) to the class of the vector with coordinates a away from x₀ and b along w, that is of (piSplitAt x₀ w hw).symm (a, b).