Theorems · Definition · category theory
CategoryTheory.LocalizerMorphism.functor
{C₁ : Type u₁} →
{C₂ : Type u₂} →
[inst : CategoryTheory.Category.{v₁, u₁} C₁] →
[inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
{W₁ : CategoryTheory.MorphismProperty C₁} →
{W₂ : CategoryTheory.MorphismProperty C₂} →
CategoryTheory.LocalizerMorphism W₁ W₂ → CategoryTheory.Functor C₁ C₂a functor between the two categories
- Cited by
- 140 results in Mathlib
- Foundations
- Depth 4 from the axioms, rests on 10 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Functorstatement · cited by 16,252
- CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
- CategoryTheory.LocalizerMorphismstatement and proof · cited by 161
Cited by186
Results whose statement or proof uses this declaration.
- CategoryTheory.LocalizerMorphism.localizedFunctorproof · cited by 29
- CategoryTheory.LocalizerMorphism.opproof · cited by 27
- CategoryTheory.LocalizerMorphism.RightResolution.wstatement · cited by 20
- CategoryTheory.LocalizerMorphism.LeftResolution.wstatement · cited by 18
- CategoryTheory.LocalizerMorphism.homMapstatement and proof · cited by 10
- CategoryTheory.LocalizerMorphism.arrowproof · cited by 9
- CategoryTheory.LocalizerMorphism.RightResolution.hwstatement · cited by 8
- CategoryTheory.LocalizerMorphism.LeftResolution.hwstatement · cited by 7
- CategoryTheory.LocalizerMorphism.Derivesproof · cited by 6
- CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparisonstatement and proof · cited by 6
- CategoryTheory.LocalizerMorphism.IsInduced.inverseImage_eqstatement · cited by 5
- CategoryTheory.LocalizerMorphism.functorialRightResolutions.ιstatement and proof · cited by 5