PastingGlobeCylinderAtoms.lean`

43 declarations, 0 contain sorry, 0 declared as axioms

Literal coefficients of the pasted-globe right cylinder

The formal endpoint and mixed bases are identified with the actual two or three Finsupp factors of each chain group. Coefficients detect equality and positivity; the basis vectors are the top chains of the constructed atoms.

abbrev OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis line 22
instance OAI.Thomason.Construction.PastingGlobeCylinderBasis.basisDecidableEq line 25
abbrev OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder line 27
def OAI.Thomason.Construction.PastingGlobeCylinderBasis.endpointCoefficient line 30
Source documentation
The coefficient in either endpoint copy.
```
def endpointCoefficient {n k : ℕ} (hkn : k < n) :
    (p : ℕ) → Bool → PastingGlobeBasis.Basis n k p → (Cylinder hkn).group p → ℤ
  | 0, a, b, x => if a then DFunLike.coe (F := PastingGlobeBasis.Chains n k 0) x.2 b
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeBasis.Chains
def OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient line 39
Source documentation
Coefficients in the actual tuple-of-Finsupp chain group.
```
def coefficient {n k p : ℕ} (hkn : k < n) : Basis n k p → (Cylinder hkn).group p → ℤ
  | .endpoint a b, x => endpointCoefficient hkn p a b x
  | .mixed b, x => DFunLike.coe (F := PastingGlobeBasis.Chains n k _) x.2.2 b
```
Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeCylinderBasis.endpointCoefficient, OAI.Thomason.Construction.PastingGlobeBasis.Chains
def OAI.Thomason.Construction.PastingGlobeCylinderBasis.vector line 44
Source documentation
The actual chain vector associated to each formal tensor basis.
```
def vector {n k p : ℕ} (hkn : k < n) : Basis n k p → (Cylinder hkn).group p
  | .endpoint a b =>
    (RightCylinder.endpoint (PastingGlobeBasis.complex n k hkn) a).app p (Finsupp.single b 1)
  | .mixed b => (0, 0, Finsupp.single b 1)

/-- Endpoint maps retain precisely the coefficient in their own copy. -/
```
Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeBasis.complex, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient
theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient_endpoint line 50
Source documentation
Endpoint maps retain precisely the coefficient in their own copy.
```
theorem coefficient_endpoint {n k p : ℕ} (hkn : k < n) (s t : Bool)
    (b : PastingGlobeBasis.Basis n k p) (x : PastingGlobeBasis.Chains n k p) :
    coefficient hkn (.endpoint t b)
        ((RightCylinder.endpoint (PastingGlobeBasis.complex n k hkn) s).app p x) =
      if t = s then x b else 0 := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeBasis.Chains, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient, OAI.Thomason.Construction.PastingGlobeBasis.complex
theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient_ext line 58
Source documentation
The formal tensor coefficients jointly detect chain equality.
```
theorem coefficient_ext {n k p : ℕ} (hkn : k < n) {x y : (Cylinder hkn).group p}
    (h : ∀ b, coefficient hkn b x = coefficient hkn b y) : x = y := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient
theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.positive_iff line 83
Source documentation
The actual positive cone is exactly coordinatewise nonnegativity.
```
theorem positive_iff {n k p : ℕ} (hkn : k < n) (x : (Cylinder hkn).group p) :
    x ∈ (Cylinder hkn).positive p ↔ ∀ b, 0 ≤ coefficient hkn b x := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient
theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient_vector line 104
Source documentation
Basis vectors have their literal Kronecker coefficients.
```
theorem coefficient_vector {n k p : ℕ} (hkn : k < n) (b c : Basis n k p) :
    coefficient hkn b (vector hkn c) = if b = c then 1 else 0 := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient, OAI.Thomason.Construction.PastingGlobeCylinderBasis.vector
def OAI.Thomason.Construction.PastingGlobeCylinderBasis.atom line 142
Source documentation
An actual bounded cell for every formal tensor basis vector.
```
def atom {n k p : ℕ} (hkn : k < n) : Basis n k p → Cell (Cylinder hkn)
  | .endpoint a b => PastingGlobeBasis.endpointAtom hkn a b
  | .mixed b => PastingGlobeBasis.mixedAtom hkn b

/-- The atom's complete top row is exactly its tensor basis vector. -/
```
Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeBasis.endpointAtom, OAI.Thomason.Construction.PastingGlobeBasis.mixedAtom
theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.atom_top line 147
Source documentation
The atom's complete top row is exactly its tensor basis vector.
```
theorem atom_top {n k p : ℕ} (hkn : k < n) (b : Basis n k p) (a : Bool) :
    (atom hkn b).table a p = vector hkn b := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.atom, OAI.Thomason.Construction.PastingGlobeCylinderBasis.vector
theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.atom_dimension line 154
Source documentation
Every chosen tensor atom is bounded by the degree of its basis vector.
```
theorem atom_dimension {n k p : ℕ} (hkn : k < n) (b : Basis n k p) :
    (Cylinder hkn).realization.DimensionLE p (atom hkn b) := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeCylinderBasis.atom
def OAI.Thomason.Construction.GridGlobeBasis.atom line 176
theorem OAI.Thomason.Construction.GridGlobeBasis.atom_top line 181
theorem OAI.Thomason.Construction.GridGlobeBasis.atom_above line 188
theorem OAI.Thomason.Construction.GridGlobeBasis.atom_below line 196
theorem OAI.Thomason.Construction.GridGlobeBasis.height_lower_false_false_false line 205
theorem OAI.Thomason.Construction.GridGlobeBasis.height_lower_false_false_true line 224
theorem OAI.Thomason.Construction.GridGlobeBasis.height_lower_false_true_false line 243
theorem OAI.Thomason.Construction.GridGlobeBasis.height_lower_false_true_true line 262
theorem OAI.Thomason.Construction.GridGlobeBasis.height_lower_true_false_false line 281
theorem OAI.Thomason.Construction.GridGlobeBasis.height_lower_true_false_true line 300
theorem OAI.Thomason.Construction.GridGlobeBasis.height_lower_true_true_false line 319
theorem OAI.Thomason.Construction.GridGlobeBasis.height_lower_true_true_true line 356
theorem OAI.Thomason.Construction.GridGlobeBasis.height_lower line 393
theorem OAI.Thomason.Construction.GridGlobeBasis.atom_sideHeight line 420
def OAI.Thomason.Construction.GridGlobeBasis.orderedAtomBasis line 433
theorem OAI.Thomason.Construction.GridGlobeBasis.orderedAtomBasis_sideHeight line 456
def OAI.Thomason.Construction.GridGlobeBasis.cylinderOrderedAtomBasis line 460
theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.endpoint_boundary_coefficient line 485
Source documentation
Endpoint boundaries stay in their chosen endpoint copy.
```
theorem endpoint_boundary_coefficient {n k p : ℕ} (hkn : k < n) (s t : Bool)
    (b : PastingGlobeBasis.Basis n k (p+1)) (c : PastingGlobeBasis.Basis n k p) :
    coefficient hkn (.endpoint t c)
        ((Cylinder hkn).differential p (vector hkn (.endpoint s b))) =
      if t = s then PastingGlobeBasis.boundary hkn b c else 0 := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeCylinderBasis.vector, OAI.Thomason.Construction.PastingGlobeBasis.boundary
theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.endpoint_mixed_boundary_coefficient line 509
Source documentation
An endpoint boundary has no mixed component.
```
theorem endpoint_mixed_boundary_coefficient {n k p : ℕ} (hkn : k < n) (s : Bool)
    (b : PastingGlobeBasis.Basis n k (p+2)) (c : PastingGlobeBasis.Basis n k p) :
    coefficient hkn (.mixed c)
        ((Cylinder hkn).differential (p+1) (vector hkn (.endpoint s b))) = 0 := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeCylinderBasis.vector
theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.mixed_endpoint_boundary_coefficient line 516
Source documentation
The endpoint part of a mixed boundary has the right-tensor sign.
```
theorem mixed_endpoint_boundary_coefficient {n k p : ℕ} (hkn : k < n) (t : Bool)
    (b c : PastingGlobeBasis.Basis n k p) :
    coefficient hkn (.endpoint t c)
        ((Cylinder hkn).differential p (vector hkn (.mixed b))) =
      (if t then (-1 : ℤ)^p else -((-1 : ℤ)^p)) * (if b = c then 1 else 0) := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeCylinderBasis.vector
theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.mixed_boundary_coefficient line 537
Source documentation
The mixed part retains the original boundary coefficients.
```
theorem mixed_boundary_coefficient {n k p : ℕ} (hkn : k < n)
    (b : PastingGlobeBasis.Basis n k (p+1)) (c : PastingGlobeBasis.Basis n k p) :
    coefficient hkn (.mixed c)
        ((Cylinder hkn).differential (p+1) (vector hkn (.mixed b))) =
      PastingGlobeBasis.boundary hkn b c := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeCylinderBasis.vector, OAI.Thomason.Construction.PastingGlobeBasis.boundary
def OAI.Thomason.Construction.PastingGlobeCylinderBasis.height line 546
Source documentation
The actual finite strong height, on all tensor degrees at once.
```
def height {n k p : ℕ} (b : Basis n k p) : ℤ :=
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis
theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.endpoint_height_lt line 549
theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.differential_height line 558
Source documentation
All negative coefficients decrease height and all positive coefficients increase it, for the literal directed-complex differential.
```
theorem differential_height {n k p : ℕ} (hkn : k < n) (a : Bool)
    (b : Basis n k (p+1)) (c : Basis n k p)
    (hc : if a then 0 < coefficient hkn c ((Cylinder hkn).differential p (vector hkn b))
      else coefficient hkn c ((Cylinder hkn).differential p (vector hkn b)) < 0) :
    if a then height b < height c else height c < height b := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeCylinderBasis.vector, OAI.Thomason.Construction.PastingGlobeCylinderBasis.height
theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.endpoint_atom_coefficient line 653
theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.mixed_atom_endpoint_coefficient line 661
theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.mixed_atom_mixed_coefficient line 679
theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.atom_lower_disjoint line 694
Source documentation
The two lower rows of every endpoint or mixed atom are disjoint.
```
theorem atom_lower_disjoint {n k p q : ℕ} (hkn : k < n) (b : Basis n k p)
    (hqp : q < p) (c : Basis n k q) :
    coefficient hkn c ((atom hkn b).table false q) = 0 ∨
      coefficient hkn c ((atom hkn b).table true q) = 0 := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient, OAI.Thomason.Construction.PastingGlobeCylinderBasis.atom
theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient_sub line 726
theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.atom_signed_table line 738
Source documentation
The complete downward-recursive signed-part formula holds for every constructed cylinder atom.
```
theorem atom_signed_table {n k p q : ℕ} (hkn : k < n) (b : Basis n k p)
    (hqp : q < p) (a : Bool) (c : Basis n k q) :
    coefficient hkn c ((atom hkn b).table a q) = max 0
      (if a then coefficient hkn c
          ((Cylinder hkn).differential q ((atom hkn b).table a (q+1)))
       else -coefficient hkn c
          ((Cylinder hkn).differential q ((atom hkn b).table a (q+1)))) := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient, OAI.Thomason.Construction.PastingGlobeCylinderBasis.atom, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder