2607.19276v1 / Norine/AntipodalModule.lean

all files

import Mathlib
import Norine.ChainObstruction

/-!
# Free antipodal modules over `F₂`

This is the algebra behind Lemma 4.7.  After a finite antipodally invariant
common refinement, polyhedral chains are ordinary coefficient functions on
the cells of that refinement.  Negation acts without fixed cells, so the norm
operator `1+A` has equal kernel and image.
-/

namespace Norine

noncomputable section

variable {α : Type*}

/-- Pull coefficient functions back along a self-map of the basis. -/
def basisPull (A : α → α) : (α → F₂) →ₗ[F₂] (α → F₂) where
  toFun f := fun a ↦ f (A a)
  map_add' f g := by
    funext a
    simp
  map_smul' r f := by
    funext a
    simp

/-- The mod-two antipodal norm on a permutation module. -/
def basisNorm (A : α → α) : (α → F₂) →ₗ[F₂] (α → F₂) :=
  LinearMap.id + basisPull A

@[simp]
theorem basisPull_apply (A : α → α) (f : α → F₂) (a : α) :
    basisPull A f a = f (A a) := rfl

@[simp]
theorem basisNorm_apply (A : α → α) (f : α → F₂) (a : α) :
    basisNorm A f a = f a + f (A a) := rfl

/-- For a fixed-point-free involution of a finite basis,
`ker(1+A) = im(1+A)`. -/
theorem basisNorm_ker_eq_range
    [Fintype α]
    (A : α → α) (hA : ∀ a, A (A a) = a) (hfree : ∀ a, A a ≠ a) :
    LinearMap.ker (basisNorm A) = LinearMap.range (basisNorm A) := by
  apply le_antisymm
  · intro f hf
    classical
    let e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
    have hinv : ∀ a, f (A a) = f a := by
      intro a
      have hker : basisNorm A f = 0 := LinearMap.mem_ker.mp hf
      have ha := congrFun hker a
      simp only [basisNorm_apply, Pi.zero_apply] at ha
      have hneg := eq_neg_of_add_eq_zero_left ha
      simpa [ZModModule.neg_eq_self] using hneg.symm
    let g : α → F₂ := fun a ↦ if e a < e (A a) then f a else 0
    refine ⟨g, ?_⟩
    funext a
    simp only [basisNorm_apply, g]
    have hne : e a ≠ e (A a) := fun h ↦ hfree a (e.injective h.symm)
    rcases lt_or_gt_of_ne hne with haa | haa
    · have hnot : ¬e (A a) < e (A (A a)) := by
        rw [hA]
        exact not_lt_of_ge haa.le
      rw [if_pos haa, if_neg hnot, add_zero]
    · have hnot : ¬e a < e (A a) := not_lt_of_ge haa.le
      have hyes : e (A a) < e (A (A a)) := by simpa [hA] using haa
      rw [if_neg hnot, if_pos hyes, zero_add, hinv]
  · intro f
    rintro ⟨g, rfl⟩
    ext a
    simp only [basisNorm_apply, hA]
    calc
      g a + g (A a) + (g (A a) + g a) =
          (g a + g a) + (g (A a) + g (A a)) := by ac_rfl
      _ = 0 := by simp [ZModModule.add_self]

/-- Elementwise form of the preceding equality, matching the hypothesis used
by `chain_level_borsuk_ulam`. -/
theorem basisNorm_exact
    [Fintype α]
    (A : α → α) (hA : ∀ a, A (A a) = a) (hfree : ∀ a, A a ≠ a)
    (f : α → F₂) (hf : basisNorm A f = 0) :
    ∃ g : α → F₂, basisNorm A g = f := by
  rw [← LinearMap.mem_range, ← basisNorm_ker_eq_range A hA hfree]
  exact hf

end

end Norine