NRR.Representation.ZeroSum — zero-sum real-valued target type (public API)

The zero-sum real-valued target type used by the perimeter test map. A value of ZeroSum n is a function Fin n → ℝ whose coordinates sum to zero. It carries the subtype topology inherited from Fin n → ℝ, a CoeFun to the underlying function, an extensionality lemma, and a Zero instance (needed so that later theorems can state that the test map vanishes, e.g. TestMap.perimeter ... s = 0).

This module keeps ZeroSum minimal: it does not introduce representation spheres, obstruction theory, or quotient spaces, and it does not make AddCommGroup/Module structure mandatory.

def NRR.ZeroSum (n : ℕ) : Type

Zero-sum real-valued target type. A function Fin n → ℝ whose coordinates sum to zero.

Equations

• NRR.ZeroSum n = { v : Fin n → ℝ // ∑ i : Fin n, v i = 0 }

@[instance_reducible]

instance NRR.instTopologicalSpaceZeroSum {n : ℕ} : TopologicalSpace (ZeroSum n)

The subtype topology inherited from Fin n → ℝ.

Equations

• NRR.instTopologicalSpaceZeroSum = instTopologicalSpaceSubtype

instance NRR.instT2SpaceZeroSum {n : ℕ} : T2Space (ZeroSum n)

The inherited topology is Hausdorff.

@[instance_reducible]

instance NRR.instCoeFunZeroSumForallFinReal {n : ℕ} : CoeFun (ZeroSum n) fun (x : ZeroSum n) => Fin n → ℝ

Coercion of a zero-sum vector to its underlying function Fin n → ℝ.

Equations

• NRR.instCoeFunZeroSumForallFinReal = { coe := fun (v : NRR.ZeroSum n) => ↑v }

@[simp]

theorem NRR.ZeroSum.sum_coe {n : ℕ} (v : ZeroSum n) : ∑ i : Fin n, ↑v i = 0

theorem NRR.ZeroSum.ext {n : ℕ} {v w : ZeroSum n} (h : ∀ (i : Fin n), ↑v i = ↑w i) : v = w

@[instance_reducible]

instance NRR.instZeroZeroSum {n : ℕ} : Zero (ZeroSum n)

The zero vector of ZeroSum n.

Equations

• NRR.instZeroZeroSum = { zero := ⟨0, ⋯⟩ }

@[simp]

theorem NRR.ZeroSum.zero_apply {n : ℕ} (i : Fin n) : ↑0 i = 0

def NRR.ZeroSum.mk' {n : ℕ} (v : Fin n → ℝ) (hv : ∑ i : Fin n, v i = 0) : ZeroSum n

Constructor for ZeroSum n from a function and a proof its coordinates sum to zero.

Equations

• NRR.ZeroSum.mk' v hv = ⟨v, hv⟩

def NRR.ZeroSum.relabel {n : ℕ} (σ : Equiv.Perm (Fin n)) (v : ZeroSum n) : ZeroSum n

Relabelling of a zero-sum vector. For a permutation σ : Equiv.Perm (Fin n) and a zero-sum vector v : ZeroSum n, the relabelled vector ZeroSum.relabel σ v is obtained by precomposing the underlying function with σ.symm, i.e. (ZeroSum.relabel σ v) i = v (σ.symm i). This σ.symm convention matches Config.relabel.

Equations

• NRR.ZeroSum.relabel σ v = ⟨fun (i : Fin n) => ↑v ((Equiv.symm σ) i), ⋯⟩

@[simp]

theorem NRR.ZeroSum.relabel_apply {n : ℕ} (σ : Equiv.Perm (Fin n)) (v : ZeroSum n) (i : Fin n) : ↑(relabel σ v) i = ↑v ((Equiv.symm σ) i)

@[simp]

theorem NRR.ZeroSum.relabel_one {n : ℕ} (v : ZeroSum n) : relabel 1 v = v

theorem NRR.ZeroSum.relabel_mul {n : ℕ} (σ τ : Equiv.Perm (Fin n)) (v : ZeroSum n) : relabel (σ * τ) v = relabel σ (relabel τ v)

@[instance_reducible]

instance NRR.instMulActionPermFinZeroSum {n : ℕ} : MulAction (Equiv.Perm (Fin n)) (ZeroSum n)

The Sₙ-action σ • v := ZeroSum.relabel σ v on the zero-sum target type, by relabelling via precomposition with σ.symm (matching the Config action convention).

Equations

• NRR.instMulActionPermFinZeroSum = { smul := fun (σ : Equiv.Perm (Fin n)) (v : NRR.ZeroSum n) => NRR.ZeroSum.relabel σ v, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem NRR.ZeroSum.smul_def {n : ℕ} (σ : Equiv.Perm (Fin n)) (v : ZeroSum n) : σ • v = relabel σ v

theorem NRR.ZeroSum.continuous_relabel {n : ℕ} (σ : Equiv.Perm (Fin n)) : Continuous fun (v : ZeroSum n) => relabel σ v

Relabelling is continuous for the subtype topology on ZeroSum n.