CountHomologyDetection.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.nonzero_of_functor_retract line 11

def OAI.DerivedBar.integerQHomologyIso line 28

Source documentation

Exact comparison of integer derived homology and the original chain degree.

def integerQHomologyIso (K : ChainComplex (ModuleCat.{u} D) ℕ) (n : ℕ) :
    (DerivedCategory.homologyFunctor (ModuleCat.{u} D) (-(n:ℤ))).obj ((integerQ D).obj K) ≅
      K.homology n :=
…

Mentions: OAI.DerivedBar.integerQ

theorem OAI.DerivedBar.ParityBridge.tensorBar_homology_zero_of_counts line 54
Source documentation
Uniform vanishing of the original count homologies implies vanishing of the entire actual balanced tensor bar, including its infinite count family.
```
theorem tensorBar_homology_zero_of_counts (n : ℕ) (h : ∀ r, IsZero ((S r).homology n)) :
    IsZero ((T).homology n) :=
…
```
theorem OAI.DerivedBar.ParityBridge.tensorBar_homology_nonzero_of_count line 60
theorem OAI.DerivedBar.ParityBridge.baseChangeTor_zero_of_counts line 68
Source documentation
Direct input bridge for uniform bounds on the original count objects in the integer derived category, yielding actual base-change Tor vanishing.
```
theorem baseChangeTor_zero_of_counts (n : ℕ)
    (h : ∀ r, IsZero ((DerivedCategory.homologyFunctor (ModuleCat D) (-(n:ℤ))).obj
      ((integerQ D).obj (S r)))) :
    IsZero (((Balanced.tensorFunctor (fstHom k D X)).leftDerived n).obj (ModuleCat.of A N)) :=
…
```
Mentions: OAI.DerivedBar.integerQ, OAI.DerivedBar.Balanced.tensorFunctor

theorem OAI.DerivedBar.ParityBridge.baseChangeTor_nonzero_of_count line 77

Source documentation

A surviving original count homology is a nonzero actual Tor group.

theorem baseChangeTor_nonzero_of_count (r n : ℕ)
    (h : ¬ IsZero ((DerivedCategory.homologyFunctor (ModuleCat D) (-(n:ℤ))).obj
      ((integerQ D).obj (S r)))) :
    ¬ IsZero (((Balanced.tensorFunctor (fstHom k D X)).leftDerived n).obj (ModuleCat.of A N)) := by
…

Mentions: OAI.DerivedBar.integerQ, OAI.DerivedBar.Balanced.tensorFunctor