CliqueCohomology.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

def OAI.EilenbergGanea.generatorExponent line 17
theorem OAI.EilenbergGanea.generatorExponent_of line 22
def OAI.EilenbergGanea.heightDifference line 27
theorem OAI.EilenbergGanea.heightDifference_commute line 30
def OAI.EilenbergGanea.cliqueSquare line 38
theorem OAI.EilenbergGanea.cliqueSquare_injective line 49
def OAI.EilenbergGanea.seedCliqueVertex line 65
def OAI.EilenbergGanea.seedCliqueEdge line 66
def OAI.EilenbergGanea.seedCliqueFace line 67
theorem OAI.EilenbergGanea.source_contains_int_square line 69
def OAI.EilenbergGanea.exponentCup line 91
Source documentation
The cup product of two integral exponent homomorphisms.
```
def exponentCup (a b : G →* Multiplicative ℤ) : cocycles₂ (Rep.trivial ℤ G ℤ) :=
…
```

theorem OAI.EilenbergGanea.exponentCup_not_coboundary line 101

Source documentation

Antisymmetrizing on a commuting pair detects a nonzero integral class.

theorem exponentCup_not_coboundary (a b : G →* Multiplicative ℤ) (g h : G)
    (hc : Commute g h)
    (hag : (a g).toAdd = 1) (hah : (a h).toAdd = 0)
    (hbg : (b g).toAdd = 0) (hbh : (b h).toAdd = 1) :
    ⇑(exponentCup a b) ∉ coboundaries₂ (Rep.trivial ℤ G ℤ) := by
…

Mentions: OAI.EilenbergGanea.exponentCup

theorem OAI.EilenbergGanea.exponentCup_class_ne_zero line 117
theorem OAI.EilenbergGanea.clique_exponent_class_nonzero line 132
theorem OAI.EilenbergGanea.cocycle_boundary_of_projectiveDimension_lt_two line 160
Source documentation
Vanishing in the literal projective-dimension sense forces every 2-cocycle in a projective resolution to be a coboundary; the fully faithful exact functor permits us to use this for the representation/group-ring equivalence.
```
theorem cocycle_boundary_of_projectiveDimension_lt_two
    [HasProjectiveDimensionLT (F.obj X) 2]
    (f : P.complex.X 2 ⟶ Y) (hf : P.complex.d 3 2 ≫ f = 0) :
    ∃ g : P.complex.X 1 ⟶ Y, P.complex.d 2 1 ≫ g = f := by
…
```
theorem OAI.EilenbergGanea.isZero_homology_two_of_projectiveDimension_lt_two line 179
Source documentation
The same vanishing expressed in the library's older linear-Yoneda model of Ext. This theorem proves rather than assumes the bridge between the two APIs.
```
theorem isZero_homology_two_of_projectiveDimension_lt_two
    (R : Type*) [Ring R] [Linear R C]
    [HasProjectiveDimensionLT (F.obj X) 2] :
    IsZero ((P.complex.linearYonedaObj R Y).homology 2) := by
…
```
theorem OAI.EilenbergGanea.two_le_cohomologicalDimension_of_H2_nonzero line 193
theorem OAI.EilenbergGanea.height_kernel_two_le_cohomologicalDimension line 211
theorem OAI.EilenbergGanea.source_two_le_cohomologicalDimension line 216