OrdinaryFunctorExtension.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.FunctorExtension.mappedSupport line 17
Source documentation
Mapping an extended complex retains its proved zero terms outside the embedded degrees.
```
theorem mappedSupport : ((F.mapHomologicalComplex c').obj (K.extend e)).IsStrictlySupported e where
…
```
def OAI.LittleFinitistic.FunctorExtension.restrictionIso line 21
Source documentation
On the actual supported degrees, mapping and extension have the same original terms.
```
def restrictionIso : ((F.mapHomologicalComplex c').obj (K.extend e)).restriction e ≅
    (F.mapHomologicalComplex c).obj K :=
…
```
def OAI.LittleFinitistic.FunctorExtension.iso line 33
Source documentation
An actual chain isomorphism commuting a zero-preserving functor with extension by zero.
```
def iso : (F.mapHomologicalComplex c').obj (K.extend e) ≅
    ((F.mapHomologicalComplex c).obj K).extend e := by
…
```