Cut profiles and the constant kernel

Lax342547.CutProfiles · concepts/Lax342547/CutProfiles.lean · lax-342547

proven

Loading review…

Natural Language Statement

Lemma

A cut profile has one coordinate for each unordered pair of tags, equal to the sum of its two representative values. In characteristic two, two representatives of the same profile differ by a constant tuple. For representatives in restricted spaces, that constant lies in their intersection. This is the kernel assertion of Lemma 2.3.

Concept map

2 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

lem✓Lax342547.CutProfiles

⊢Lax342547Proofs.CutProfiles.same_cut_iff

Lean source view on GitHub

Show types on hover

1	import Lax342547.MomentSpace
2	import Mathlib.LinearAlgebra.Pi
3
4	/-!
5	---
6	title: Cut profiles and the constant kernel
7	type: lemma
8	---
9	A cut profile has one coordinate for each unordered pair of tags, equal
10	to the sum of its two representative values. In characteristic two,
11	two representatives of the same profile differ by a constant tuple.
12	For representatives in restricted spaces, that constant lies in their
13	intersection. This is the kernel assertion of Lemma 2.3.
14	-/
15
16	namespace Lax342547.CutProfiles
17
18	open Lax342547.MomentSpace
19
20	def Component (Tag : Type) := {e : Finset Tag // e.card = 2}
21
22	variable {Tag V : Type} [AddCommGroup V] [Module Binary V]
23
24	def cutMap : (Tag → V) →ₗ[Binary] (Component Tag → V) where
25	toFun w e := ∑ t ∈ e.val, w t
26	map_add' w v := by ext e; simp [Finset.sum_add_distrib]
27	map_smul' c w := by ext e; simp [Finset.smul_sum]
28
29	def representatives (W : Tag → Submodule Binary V) : Submodule Binary (Tag → V) :=
30	Submodule.pi Set.univ W
31
32	def cutSpace (W : Tag → Submodule Binary V) : Submodule Binary (Component Tag → V) :=
33	(representatives W).map cutMap
34
35	axiom same_cut_iff [Nonempty Tag] (W : Tag → Submodule Binary V)
36	(w v : Tag → V) (hw : ∀ t, w t ∈ W t) (hv : ∀ t, v t ∈ W t) :
37	cutMap w = cutMap v ↔ ∃ c ∈ ⨅ t, W t, ∀ t, w t + v t = c
38
39	end Lax342547.CutProfiles
40