CanonicalArrowCompatibility.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.LittleFinitistic.CanonicalArrowCompatibility.diagonal_original line 14
lemma OAI.LittleFinitistic.CanonicalArrowCompatibility.arrow01_target line 26
lemma OAI.LittleFinitistic.CanonicalArrowCompatibility.arrow12_target line 31
def OAI.LittleFinitistic.CanonicalArrowCompatibility.arrow01Map line 37
Source documentation
Left multiplication by the original first arrow on the actual vertex complexes.
```
def arrow01Map (a : Fin (d+1)) :=
…
```
def OAI.LittleFinitistic.CanonicalArrowCompatibility.arrow12Map line 43
Source documentation
Left multiplication by the original second arrow on the actual vertex complexes.
```
def arrow12Map (b : Fin (d+1)) :=
…
```
def OAI.LittleFinitistic.CanonicalArrowCompatibility.compatibility01 line 49
Source documentation
The homotopy uses exactly the original first and second vertex equivalences.
```
def compatibility01 (a : Fin (d+1)) : Homotopy
    (FirstVertex.iota P D₀ D₁ D₂ f g H ≫ arrow01Map P D₀ D₁ D₂ f g H a)
    (f a ≫ SecondVertex.iota P D₀ D₁ D₂ f g H) := by
…
```
Mentions: OAI.LittleFinitistic.FirstVertex.iota, OAI.LittleFinitistic.CanonicalArrowCompatibility.arrow01Map, OAI.LittleFinitistic.SecondVertex.iota
def OAI.LittleFinitistic.CanonicalArrowCompatibility.compatibility12 line 59
Source documentation
The homotopy uses exactly the original second and third vertex equivalences.
```
def compatibility12 (b : Fin (d+1)) : Homotopy
    (SecondVertex.iota P D₀ D₁ D₂ f g H ≫ arrow12Map P D₀ D₁ D₂ f g H b)
    (g b ≫ ThirdVertex.iota P D₀ D₁ D₂ f g H) := by
…
```
Mentions: OAI.LittleFinitistic.SecondVertex.iota, OAI.LittleFinitistic.CanonicalArrowCompatibility.arrow12Map, OAI.LittleFinitistic.ThirdVertex.iota