The finite charts component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.PaperFiniteCharts.F : Type

The F construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFiniteCharts.F = Connes.Construction.k

@[reducible, inline]

abbrev Connes.PaperFiniteCharts.R : Type

The R construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFiniteCharts.R = Connes.Construction.R

@[reducible, inline]

abbrev Connes.PaperFiniteCharts.A : Type

The A construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFiniteCharts.A = Connes.Construction.A

@[reducible, inline]

abbrev Connes.PaperFiniteCharts.C : Submodule Construction.k Construction.PaperKernel.TensorAA

The C construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFiniteCharts.C = Connes.Construction.PaperKernel.C

@[instance_reducible]

noncomputable instance Connes.PaperFiniteCharts.paperFintype : Fintype F

Equations

• Connes.PaperFiniteCharts.paperFintype = inferInstance

noncomputable def Connes.PaperFiniteCharts.polynomialChart (N : ℕ) : Finset R

The polynomialChart construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFiniteCharts.polynomialChart N = Finset.image (⇑(Polynomial.ofFn N)) Finset.univ

theorem Connes.PaperFiniteCharts.mem_polynomialChart_iff (N : ℕ) (p : R) : p ∈ polynomialChart N ↔ ∃ (v : Fin N → F), (Polynomial.ofFn N) v = p

theorem Connes.PaperFiniteCharts.polynomialChart_card (N : ℕ) : (polynomialChart N).card = Fintype.card (Fin N → F)

def Connes.PaperFiniteCharts.extendCoefficients {N M : ℕ} (_hNM : N ≤ M) (v : Fin N → F) : Fin M → F

Coefficient extension preserves the represented polynomial. Paper: Lemma 4.2.

Equations

• Connes.PaperFiniteCharts.extendCoefficients _hNM v i = if hi : ↑i < N then v ⟨↑i, hi⟩ else 0

theorem Connes.PaperFiniteCharts.ofFn_extendCoefficients {N M : ℕ} (hNM : N ≤ M) (v : Fin N → F) : (Polynomial.ofFn M) (extendCoefficients hNM v) = (Polynomial.ofFn N) v

theorem Connes.PaperFiniteCharts.polynomialChart_mono {N M : ℕ} (hNM : N ≤ M) : polynomialChart N ⊆ polynomialChart M

def Connes.PaperFiniteCharts.next (s : Fin 3) : Fin 3

The cyclic coordinate order used for the three paper charts. Paper: Lemma 4.2.

Equations

• Connes.PaperFiniteCharts.next s = ⟨(↑s + 1) % 3, ⋯⟩

def Connes.PaperFiniteCharts.nextNext (s : Fin 3) : Fin 3

The nextNext construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFiniteCharts.nextNext s = Connes.PaperFiniteCharts.next (Connes.PaperFiniteCharts.next s)

theorem Connes.PaperFiniteCharts.next_ne (s : Fin 3) : next s ≠ s

theorem Connes.PaperFiniteCharts.nextNext_ne (s : Fin 3) : nextNext s ≠ s

theorem Connes.PaperFiniteCharts.next_nextNext_ne (s : Fin 3) : next s ≠ nextNext s

noncomputable def Connes.PaperFiniteCharts.basisVector (s : Fin 3) : A

The standard basis vector in A. Paper: Lemma 4.2.

Equations

• Connes.PaperFiniteCharts.basisVector s = Pi.single s 1

noncomputable def Connes.PaperFiniteCharts.chartVector (s : Fin 3) (f h : R) : A

A point in one of the three finite charts. Paper: Lemma 4.2.

Equations

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

@[reducible, inline]

abbrev Connes.PaperFiniteCharts.ChartIndex (N : ℕ) : Type

The ChartIndex construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFiniteCharts.ChartIndex N = (Fin 3 × (Fin N → Connes.PaperFiniteCharts.F) × (Fin N → Connes.PaperFiniteCharts.F))

noncomputable def Connes.PaperFiniteCharts.chartPoint (N : ℕ) (i : ChartIndex N) : A

The chartPoint construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFiniteCharts.chartPoint N i = Connes.PaperFiniteCharts.chartVector i.1 ((Polynomial.ofFn N) i.2.1) ((Polynomial.ofFn N) i.2.2)

noncomputable def Connes.PaperFiniteCharts.chartSquare (N : ℕ) (i : ChartIndex N) : ↥C

The chartSquare construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFiniteCharts.chartSquare N i = Connes.Construction.PaperKernel.diagonal (Connes.PaperFiniteCharts.chartPoint N i)

noncomputable def Connes.PaperFiniteCharts.chartSubmodule (N : ℕ) : Submodule Construction.k ↥C

The chart span C_N. Paper: Lemma 4.2.

Equations

• Connes.PaperFiniteCharts.chartSubmodule N = Submodule.span Connes.Construction.k (Set.range (Connes.PaperFiniteCharts.chartSquare N))

def Connes.PaperFiniteCharts.polynomialBasis (N : ℕ) (i : Fin N) : R

Coordinate basis for the two polynomial parameters. Paper: Lemma 4.2.

Equations

• Connes.PaperFiniteCharts.polynomialBasis N i = (Polynomial.ofFn N) (Pi.single i 1)

theorem Connes.PaperFiniteCharts.ofFn_eq_sum_polynomialBasis (N : ℕ) (v : Fin N → F) : (Polynomial.ofFn N) v = ∑ i : Fin N, v i • polynomialBasis N i

@[reducible, inline]

abbrev Connes.PaperFiniteCharts.CoeffIndex (N : ℕ) : Type

The CoeffIndex construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFiniteCharts.CoeffIndex N = (Fin N ⊕ Fin N)

noncomputable def Connes.PaperFiniteCharts.coefficientVector (N : ℕ) (s : Fin 3) : CoeffIndex N → A

The coefficientVector construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFiniteCharts.coefficientVector N s (Sum.inl i) = Connes.PaperFiniteCharts.polynomialBasis N i • Connes.PaperFiniteCharts.basisVector (Connes.PaperFiniteCharts.next s)
• Connes.PaperFiniteCharts.coefficientVector N s (Sum.inr i) = Connes.PaperFiniteCharts.polynomialBasis N i • Connes.PaperFiniteCharts.basisVector (Connes.PaperFiniteCharts.nextNext s)

theorem Connes.PaperFiniteCharts.chartPoint_eq_affine_sum (N : ℕ) (s : Fin 3) (f h : Fin N → F) : chartPoint N (s, f, h) = basisVector s + ∑ i : Fin N, f i • coefficientVector N s (Sum.inl i) + ∑ i : Fin N, h i • coefficientVector N s (Sum.inr i)

theorem Connes.PaperFiniteCharts.chartPoint_apply_self (N : ℕ) (s : Fin 3) (f h : Fin N → F) : chartPoint N (s, f, h) s = 1

theorem Connes.PaperFiniteCharts.chartPoint_mem_span (N : ℕ) (i : ChartIndex N) : chartSquare N i ∈ chartSubmodule N

theorem Connes.PaperFiniteCharts.chartSubmodule_mono {N M : ℕ} (hNM : N ≤ M) : chartSubmodule N ≤ chartSubmodule M

theorem Connes.PaperFiniteCharts.polynomial_mem_some_chart (p : R) : ∃ (N : ℕ), p ∈ polynomialChart N