ResolutionDerived.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DerivedBar.resolution_map_isIso line 15
def OAI.DerivedBar.resolutionLiftUp line 19
Source documentation
A candidate map into the resolved model, before descending the localization.
```
def resolutionLiftUp (G : E ⥤ H) (β : L ⋙ G ⟶ F) : L ⋙ G ⟶ L ⋙ LF := by
…
```
def OAI.DerivedBar.resolutionLift line 28
Source documentation
Full faithfulness of precomposition by the localization descends that map.
```
def resolutionLift (G : E ⥤ H) (β : L ⋙ G ⟶ F) : G ⟶ LF :=
…
```
lemma OAI.DerivedBar.whisker_resolutionLift line 32
lemma OAI.DerivedBar.resolutionLift_fac line 38
lemma OAI.DerivedBar.resolutionLift_unique line 50
theorem OAI.DerivedBar.isLeftDerivedFunctor_of_resolution line 70
Source documentation
A functorial resolution computes the genuine left derived functor. The criterion is a right Kan extension universal property; its hypotheses are checked on the actual bar resolution in the application.
```
theorem isLeftDerivedFunctor_of_resolution : LF.IsLeftDerivedFunctor α W where
…
```