Documentation Verification Report

Derives

📁 Source: Mathlib/CategoryTheory/Localization/DerivabilityStructure/Derives.lean

Statistics

Metric	Count
Definitions `Derives`, `Derives`	2
Theorems `hasPointwiseRightDerivedFunctor`, `isIso`, `isRightDerivedFunctor_iff_isIso`, `isRightDerivedFunctor_of_isIso`	4
Total	6

CategoryTheory.LocalizerMorphism

Definitions

Name	Category	Theorems
`Derives` 📖	MathDef	—

CategoryTheory.LocalizerMorphism.Derives

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasPointwiseRightDerivedFunctor` 📖	mathematical	`CategoryTheory.LocalizerMorphism.Derives`	`CategoryTheory.Functor.HasPointwiseRightDerivedFunctor`	—	`CategoryTheory.LocalizerMorphism.hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure` `CategoryTheory.Functor.hasPointwiseRightDerivedFunctor_of_inverts`
`isIso` 📖	mathematical	`CategoryTheory.LocalizerMorphism.Derives`	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.LocalizerMorphism.functor` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app`	—	`CategoryTheory.Functor.q_isLocalization` `CategoryTheory.Functor.isRightDerivedFunctor_of_inverts` `CategoryTheory.Functor.hasPointwiseRightDerivedFunctor_of_inverts` `CategoryTheory.LocalizerMorphism.isIso_iff_of_isRightDerivabilityStructure` `CategoryTheory.NatIso.inv_app_isIso`
`isRightDerivedFunctor_iff_isIso` 📖	mathematical	`CategoryTheory.LocalizerMorphism.Derives`	`CategoryTheory.Functor.IsRightDerivedFunctor` `CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.LocalizerMorphism.functor` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app`	—	`isIso` `isRightDerivedFunctor_of_isIso`
`isRightDerivedFunctor_of_isIso` 📖	mathematical	`CategoryTheory.LocalizerMorphism.Derives` `CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.LocalizerMorphism.functor` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app`	`CategoryTheory.Functor.IsRightDerivedFunctor`	—	`hasPointwiseRightDerivedFunctor` `CategoryTheory.Functor.hasRightDerivedFunctor_of_hasPointwiseRightDerivedFunctor` `isIso` `CategoryTheory.LocalizerMorphism.essSurj_of_hasRightResolutions` `CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.hasRightResolutions` `CategoryTheory.Functor.instIsRightDerivedFunctorTotalRightDerivedTotalRightDerivedUnit` `CategoryTheory.Functor.rightDerived_fac` `CategoryTheory.NatTrans.isIso_iff_isIso_app` `CategoryTheory.NatTrans.isIso_app_iff_of_iso` `CategoryTheory.Functor.isRightDerivedFunctor_iff_of_iso`

ContextFreeGrammar

Definitions

Name	Category	Theorems
`Derives` 📖	MathDef	8 math math: `Produces.single`, `Derives.refl`, `mem_language_iff`, `derives_reverse_comm`, `derives_iff_eq_or_tail`, `derives_reverse`, `derives_iff_eq_or_head`, `derives_nonterminal`

---

← Back to Index