IntegerExtensionFunctor.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.IntegerExtensionFunctor.termIso line 15

Source documentation

Additive functors preserve the zero components added by integer extension.

def termIso : (o : Option ℕ) → F.obj (HomologicalComplex.extend.X Z o) ≅
    HomologicalComplex.extend.X ((F.mapHomologicalComplex c).obj Z) o
  | none => (F.map_isZero (isZero_zero _)).iso (isZero_zero _)
  | some _ => Iso.refl _

theorem OAI.LittleFinitistic.IntegerExtensionFunctor.termIso_d line 20
def OAI.LittleFinitistic.IntegerExtensionFunctor.complexIso line 28
Source documentation
Applying an additive module functor commutes with the actual n ↦ -n zero extension.
```
def complexIso : (F.mapHomologicalComplex (.up ℤ)).obj ((DerivedBar.integerExtension B).obj Z) ≅
    (DerivedBar.integerExtension B).obj ((F.mapHomologicalComplex c).obj Z) :=
…
```
Mentions: OAI.DerivedBar.integerExtension
theorem OAI.LittleFinitistic.IntegerExtensionFunctor.termIso_natural line 34
def OAI.LittleFinitistic.IntegerExtensionFunctor.naturalIso line 42
Source documentation
Naturality holds on every chain map, including the added zero degrees.
```
def naturalIso : DerivedBar.integerExtension B ⋙ F.mapHomologicalComplex (.up ℤ) ≅
    F.mapHomologicalComplex c ⋙ DerivedBar.integerExtension B :=
…
```
Mentions: OAI.DerivedBar.integerExtension