TwoDegreeFormalityNaturality.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LittleFinitistic.TwoDegreeFormality.modelMap line 14
lemma OAI.LittleFinitistic.TwoDegreeFormality.braiding_square line 18
lemma OAI.LittleFinitistic.TwoDegreeFormality.stalk_diagonal_square line 25
theorem OAI.LittleFinitistic.TwoDegreeFormality.splitIso_naturality line 38
Source documentation
The actual two-degree formality isomorphism is natural for all derived B-morphisms.
```
theorem splitIso_naturality :
    f ≫ (splitIso P Y hY).hom = (splitIso P X hX).hom ≫ modelMap P f := by
…
```
Mentions: OAI.LittleFinitistic.TwoDegreeFormality.splitIso, OAI.LittleFinitistic.TwoDegreeFormality.modelMap
theorem OAI.LittleFinitistic.TwoDegreeFormality.splitIso_endomorphism line 55
Source documentation
In particular every endomorphism acts diagonally by its two actual cohomology maps.
```
theorem splitIso_endomorphism (a : End X) :
    a ≫ (splitIso P X hX).hom = (splitIso P X hX).hom ≫ modelMap P a :=
…
```
Mentions: OAI.LittleFinitistic.TwoDegreeFormality.splitIso, OAI.LittleFinitistic.TwoDegreeFormality.modelMap
theorem OAI.LittleFinitistic.TwoDegreeFormality.splitIso_action line 60
Source documentation
The splitting retains any specified action by derived B-linear endomorphisms.
```
theorem splitIso_action (S : Type w) [Monoid S] (rho : S →* End X) (r : S) :
    rho r ≫ (splitIso P X hX).hom = (splitIso P X hX).hom ≫ modelMap P (rho r) :=
…
```
Mentions: OAI.LittleFinitistic.TwoDegreeFormality.splitIso, OAI.LittleFinitistic.TwoDegreeFormality.modelMap
def OAI.LittleFinitistic.TwoDegreeFormality.splitIsoWithModels line 65
Source documentation
Substitute actual B-module identifications of the two cohomology modules.
```
def splitIsoWithModels (M N : C.{u,v} P) (e0 : H P 0 X ≅ M) (em : H P (-3) X ≅ N) :
    X ≅ stalk P M ⊞ (stalk P N)⟦(3 : ℤ)⟧ :=
…
```
Mentions: OAI.LittleFinitistic.TwoDegreeFormality.H, OAI.LittleFinitistic.TwoDegreeFormality.stalk