FiniteParity.lean`

53 declarations, 0 contain sorry, 0 declared as axioms

Finite parity for the PL continuation argument. The argument constructs continuation without assuming a topological degree theorem.

lemma OAI.SharpLiebThirring.PLParity.affine_constraints_endpoints line 19

Source documentation

Endpoints of a line meeting a simplex: in general position either no facet, or exactly two facets, are met. The roots r are the facet crossing parameters.

lemma affine_constraints_endpoints {ι : Type u40} [Fintype ι] [DecidableEq ι]
    (b r : ι → ℝ) (hb : ∀ i, b i ≠ 0) (hr : Function.Injective r)
    (hpos : ∃ i, 0 < b i) (hneg : ∃ i, b i < 0) :
    ∃ i j : ι, i ≠ j ∧
      ({k | ∀ l, 0 ≤ b l * (r k - r l)} : Finset ι) =
        if r i < r j then {i, j} else ∅ := by
…

lemma OAI.SharpLiebThirring.PLParity.even_affine_constraints_endpoints line 80
def OAI.SharpLiebThirring.PLParity.augmentedMap line 95
Source documentation
Total affine weights and their vector sum.
```
def augmentedMap (v : ι → V) : (ι → ℝ) →ₗ[ℝ] ℝ × V where
…
```
lemma OAI.SharpLiebThirring.PLParity.augmentedMap_apply line 100
def OAI.SharpLiebThirring.PLParity.facetHit line 104
Source documentation
A facet is selected when its affine image contains zero.
```
def facetHit (v : ι → V) (i : ι) : Prop :=
…
```
lemma OAI.SharpLiebThirring.PLParity.facetHit_congr line 107
lemma OAI.SharpLiebThirring.PLParity.facetHit_linearEquiv line 127
lemma OAI.SharpLiebThirring.PLParity.kernel_line_parameterization line 141

lemma OAI.SharpLiebThirring.PLParity.even_facetHit_of_kernel_line line 160

Source documentation

Parity of facet hits for a generic affine map from a (d+1)-simplex to R^d. The algebraic general-position conditions are separated from the finite counting argument so they can be supplied by generic vertex choices.

lemma even_facetHit_of_kernel_line (v : ι → V)
    (hsur : Function.Surjective (augmentedMap v))
    (hdim : Module.finrank ℝ (LinearMap.ker (augmentedMap v)) = 1)
    (hcoord : ∀ b : ι → ℝ, augmentedMap v b = 0 → b ≠ 0 → ∀ i, b i ≠ 0)
    (hpair : ∀ w : ι → ℝ, augmentedMap v w = (1, 0) →
      ∀ i j, w i = 0 → w j = 0 → i = j) :
    Even ({i | facetHit v i} : Finset ι).card := by
…

Mentions: OAI.SharpLiebThirring.PLParity.augmentedMap, OAI.SharpLiebThirring.PLParity.facetHit

lemma OAI.SharpLiebThirring.PLParity.sum_subtype_eq_of_zero line 228
lemma OAI.SharpLiebThirring.PLParity.augmentedMap_single line 235
lemma OAI.SharpLiebThirring.PLParity.augmented_kernel_nonzero_coordinates line 240
lemma OAI.SharpLiebThirring.PLParity.augmented_nonzero_two_coordinates line 260
lemma OAI.SharpLiebThirring.PLParity.facetHit_positive line 285
lemma OAI.SharpLiebThirring.PLParity.augmentedMap_surjective line 298
lemma OAI.SharpLiebThirring.PLParity.even_facetHit line 319
lemma OAI.SharpLiebThirring.PLParity.orbit_mk_smul line 348
def OAI.SharpLiebThirring.PLParity.orbitProductEquiv line 353
Source documentation
Reconstruct a point in a free orbit from its representative and a group element.
```
def orbitProductEquiv : (Quotient (MulAction.orbitRel G X) × G) ≃ X :=
…
```
lemma OAI.SharpLiebThirring.PLParity.sum_eq_card_mul_orbit_sum line 371
def OAI.SharpLiebThirring.PLParity.rowDegree line 386
def OAI.SharpLiebThirring.PLParity.colDegree line 387
lemma OAI.SharpLiebThirring.PLParity.rowDegree_invariant line 390
lemma OAI.SharpLiebThirring.PLParity.colDegree_invariant line 397
lemma OAI.SharpLiebThirring.PLParity.sum_rowDegree_eq_sum_colDegree line 403
lemma OAI.SharpLiebThirring.PLParity.even_odd_degree_orbits line 413
Source documentation
The number of odd-degree facet orbits is even whenever every top-cell has even degree. This is the equivariant handshaking lemma: the action must be free, but neither the base nor the target needs an orientation.
```
lemma even_odd_degree_orbits (R : T → F → Prop)
    (hR : ∀ g : G, ∀ t f, R (g • t) (g • f) ↔ R t f)
    (hEven : ∀ t, Even (rowDegree R t)) :
    Even ({q : Quotient (MulAction.orbitRel G F) | Odd (colDegree R q.out)} :
      Finset (Quotient (MulAction.orbitRel G F))).card := by
…
```
Mentions: OAI.SharpLiebThirring.PLParity.rowDegree, OAI.SharpLiebThirring.PLParity.colDegree
lemma OAI.SharpLiebThirring.PLParity.even_orbit_card_of_even_fibers line 433
lemma OAI.SharpLiebThirring.PLParity.orbit_map_respects line 447

def OAI.SharpLiebThirring.PLParity.orbitMap line 457

Source documentation

An equivariant involution descends to orbit classes.

def orbitMap (f : H → H) (hf : ∀ g : G, ∀ h, f (g • h) = g • f h) :
    Quotient (MulAction.orbitRel G H) → Quotient (MulAction.orbitRel G H) :=
…

lemma OAI.SharpLiebThirring.PLParity.orbitMap_involutive line 463
lemma OAI.SharpLiebThirring.PLParity.even_fixedPoints_of_even_card line 471

lemma OAI.SharpLiebThirring.PLParity.exists_other_fixed_orbit line 486

Source documentation

One initial crossing orbit cannot be the only fixed orbit of an equivariant half-edge pairing; a second boundary crossing orbit must exist.

lemma exists_other_fixed_orbit (p : H → T)
    (hp : ∀ g : G, ∀ h, p (g • h) = g • p h)
    (hEven : ∀ t, Even (Nat.card {h // p h = t}))
    (f : H → H) (hf : ∀ g : G, ∀ h, f (g • h) = g • f h)
    (hi : Function.Involutive f)
    (q₀ : Quotient (MulAction.orbitRel G H)) (hq₀ : orbitMap f hf q₀ = q₀) :
    ∃ q : Quotient (MulAction.orbitRel G H), orbitMap f hf q = q ∧ q ≠ q₀ := by
…

Mentions: OAI.SharpLiebThirring.PLParity.orbitMap

structure OAI.SharpLiebThirring.PLParity.FinitePairing.CellFacet line 517
instance OAI.SharpLiebThirring.PLParity.FinitePairing.(instance at line 521) line 521
instance OAI.SharpLiebThirring.PLParity.FinitePairing.(instance at line 525) line 525
instance OAI.SharpLiebThirring.PLParity.FinitePairing.(instance at line 536) line 536
def OAI.SharpLiebThirring.PLParity.FinitePairing.selected line 550
Source documentation
Selected simplex-facet incidences in a finite invariant domain.
```
def selected : SubMulAction G (CellFacet D J) where
…
```
Mentions: OAI.SharpLiebThirring.PLParity.FinitePairing.CellFacet
instance OAI.SharpLiebThirring.PLParity.FinitePairing.selectedFintype line 554
def OAI.SharpLiebThirring.PLParity.FinitePairing.pairing line 558
Source documentation
Pair an interior selected facet with its neighbor, and keep boundary facets fixed.
```
def pairing (p : selected D hit hHit) : selected D hit hHit :=
…
```
Mentions: OAI.SharpLiebThirring.PLParity.FinitePairing.selected
lemma OAI.SharpLiebThirring.PLParity.FinitePairing.pairing_boundary line 564
lemma OAI.SharpLiebThirring.PLParity.FinitePairing.pairing_involutive line 570
lemma OAI.SharpLiebThirring.PLParity.FinitePairing.pairing_equivariant line 583
lemma OAI.SharpLiebThirring.PLParity.FinitePairing.selected_projection_equivariant line 599
lemma OAI.SharpLiebThirring.PLParity.FinitePairing.even_projection_fiber line 602

lemma OAI.SharpLiebThirring.PLParity.FinitePairing.exists_other_boundary line 622

Source documentation

In a free finite equivariant complex with even selected facet counts, a boundary crossing orbit forces another boundary crossing orbit.

lemma exists_other_boundary [Fintype D] [Fintype J] [Fintype G] [IsCancelSMul G X]
    (hEven : ∀ x : D, Even (Nat.card {j // hit x.val j}))
    (hNoOrbit : ∀ x : D, ∀ j, nbr x.val j ∈ D → ∀ g : G, nbr x.val j ≠ g • x.val)
    (p₀ : selected D hit hHit) (hp₀ : nbr p₀.val.cell.val p₀.val.facet ∉ D) :
    ∃ p : selected D hit hHit, nbr p.val.cell.val p.val.facet ∉ D ∧
      ¬ (MulAction.orbitRel G (selected D hit hHit)) p p₀ := by
…

Mentions: OAI.SharpLiebThirring.PLParity.FinitePairing.selected

def OAI.SharpLiebThirring.CubeFlags.extendValues line 666
Source documentation
Extend finite equivariant vertex data by zero outside the invariant complex.
```
def extendValues (a : vertices H D → V) (z : Fin n → ℤ) : V :=
…
```
Mentions: OAI.SharpLiebThirring.CubeFlags.vertices
lemma OAI.SharpLiebThirring.CubeFlags.extendValues_at line 670
lemma OAI.SharpLiebThirring.CubeFlags.extendValues_equivariant line 676
def OAI.SharpLiebThirring.CubeFlags.cellHit line 686
lemma OAI.SharpLiebThirring.CubeFlags.cellHit_equivariant line 690
lemma OAI.SharpLiebThirring.CubeFlags.cellHit_neighbor line 702
lemma OAI.SharpLiebThirring.CubeFlags.cellHit_even line 709
lemma OAI.SharpLiebThirring.CubeFlags.neighbor_not_orbit line 720

lemma OAI.SharpLiebThirring.CubeFlags.another_boundary line 735

Source documentation

The geometric complex now satisfies the abstract mod-two boundary lemma.

lemma another_boundary [Fintype D] (a : vertices H D → V)
    (ha : ∀ s : H, ∀ z, a (s • z) = ρ s (a z)) (hc : n = Module.finrank ℝ V + 1)
    (haug : ∀ F : D, ∀ j : Fin (n + 1), LinearIndependent ℝ
      (fun k : {k // k ≠ j} ↦ ((1 : ℝ), a (flagVertex H D F k))))
    (hvec : ∀ F : D, ∀ i j : Fin (n + 1), i ≠ j → LinearIndependent ℝ
      (fun k : {k // k ≠ i ∧ k ≠ j} ↦ a (flagVertex H D F k)))
    (h : ℝ) (hfree : ∀ z : vertices H D, ∀ s : H,
      s • gridPoint h z.val = gridPoint h z.val → s = 1)
    (p₀ : FinitePairing.selected D (cellHit H D a) (cellHit_equivariant H D ρ a ha))
    (hp₀ : p₀.val.cell.val.neighbor p₀.val.facet ∉ D) :
    ∃ p : FinitePairing.selected D (cellHit H D a) (cellHit_equivariant H D ρ a ha),
      p.val.cell.val.neighbor p.val.facet ∉ D ∧
…

Mentions: OAI.SharpLiebThirring.CubeFlags.vertices, OAI.SharpLiebThirring.CubeFlags.flagVertex, OAI.SharpLiebThirring.CubeFlags.gridPoint, OAI.SharpLiebThirring.CubeFlags.cellHit, OAI.SharpLiebThirring.CubeFlags.cellHit_equivariant