The concrete right-coordinate model for a stage

The iterated Ore tower currently supplies nested additive normal forms, but it does not yet identify a localized stage with a free right module over its coefficient stage. This file formalizes the part that is unconditional and used once that identification is available: the canonical coordinatewise right action on the free coordinate object ι →₀ S, together with its finite single-coordinate decomposition. No freeness of an Ore localization is assumed or encoded by an equivalent hypothesis here.

noncomputable def AlgebraicAnalysis.RightCoordinates.rightCoordinateAction {S : Type u_1} {ι : Type u_2} [Ring S] (v : ι →₀ S) (a : S) : ι →₀ S

The coordinatewise right action on finitely supported S-coordinates.

Equations

• AlgebraicAnalysis.RightCoordinates.rightCoordinateAction v a = MulOpposite.op a • v

@[simp]

theorem AlgebraicAnalysis.RightCoordinates.rightCoordinateAction_apply {S : Type u_1} {ι : Type u_2} [Ring S] (v : ι →₀ S) (a : S) (i : ι) : (rightCoordinateAction v a) i = v i * a

@[simp]

theorem AlgebraicAnalysis.RightCoordinates.rightCoordinateAction_eq_op_smul {S : Type u_1} {ι : Type u_2} [Ring S] (v : ι →₀ S) (a : S) : rightCoordinateAction v a = MulOpposite.op a • v

theorem AlgebraicAnalysis.RightCoordinates.rightCoordinateAction_add {S : Type u_1} {ι : Type u_2} [Ring S] (v w : ι →₀ S) (a : S) : rightCoordinateAction (v + w) a = rightCoordinateAction v a + rightCoordinateAction w a

Coordinatewise right multiplication is additive in the vector.

theorem AlgebraicAnalysis.RightCoordinates.rightCoordinateAction_add_scalar {S : Type u_1} {ι : Type u_2} [Ring S] (v : ι →₀ S) (a b : S) : rightCoordinateAction v (a + b) = rightCoordinateAction v a + rightCoordinateAction v b

Coordinatewise right multiplication is additive in the scalar.

theorem AlgebraicAnalysis.RightCoordinates.rightCoordinateAction_one {S : Type u_1} {ι : Type u_2} [Ring S] (v : ι →₀ S) : rightCoordinateAction v 1 = v

theorem AlgebraicAnalysis.RightCoordinates.rightCoordinateAction_mul {S : Type u_1} {ι : Type u_2} [Ring S] (v : ι →₀ S) (a b : S) : rightCoordinateAction (rightCoordinateAction v a) b = rightCoordinateAction v (a * b)

Written in right-sided order, successive coordinate actions multiply the scalars in the same order.

theorem AlgebraicAnalysis.RightCoordinates.rightCoordinateAction_sum {S : Type u_1} {ι : Type u_2} {α : Type u_3} [Ring S] (t : Finset α) (f : α → ι →₀ S) (a : S) : rightCoordinateAction (∑ j ∈ t, f j) a = ∑ j ∈ t, rightCoordinateAction (f j) a

Coordinatewise right multiplication commutes with finite additive sums.

theorem AlgebraicAnalysis.RightCoordinates.rightCoordinateAction_single {S : Type u_1} {ι : Type u_2} [Ring S] (i : ι) (s a : S) : rightCoordinateAction (Finsupp.single i s) a = Finsupp.single i (s * a)

A single coordinate remains a single coordinate under the right action.

theorem AlgebraicAnalysis.RightCoordinates.rightCoordinate_decomposition {S : Type u_1} {ι : Type u_2} [Ring S] (v : ι →₀ S) : v = ∑ i ∈ v.support, Finsupp.single i (v i)

Every finitely supported coordinate vector is the finite sum of its pure coordinate vectors.

theorem AlgebraicAnalysis.RightCoordinates.rightCoordinate_decomposition_action {S : Type u_1} {ι : Type u_2} [Ring S] (v : ι →₀ S) (a : S) : rightCoordinateAction v a = ∑ i ∈ v.support, Finsupp.single i (v i * a)

After a right action, the finite coordinate decomposition is acted on coordinatewise.

theorem AlgebraicAnalysis.RightCoordinates.rightCoordinate_eq_top_of_single_mem {S : Type u_1} {ι : Type u_2} [Ring S] (H : Submodule Sᵐᵒᵖ (ι →₀ S)) (hH : ∀ (i : ι) (s : S), Finsupp.single i s ∈ H) : H = ⊤

The canonical pure coordinates generate the free right-coordinate model.