Theorems · Definition · category theory
CategoryTheory.Localization.Construction.lift
{C : Type uC} →
[inst : CategoryTheory.Category.{uC', uC} C] →
{W : CategoryTheory.MorphismProperty C} →
{D : Type uD} →
[inst_1 : CategoryTheory.Category.{uD', uD} D] →
(G : CategoryTheory.Functor C D) → W.IsInvertedBy G → CategoryTheory.Functor W.Localization DThe lifting of a functor C ⥤ D inverting W as a functor W.Localization ⥤ D
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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 and proof · cited by 16,252
- CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
- CategoryTheory.MorphismProperty.IsInvertedBystatement and proof · cited by 118
- CategoryTheory.MorphismProperty.Localizationstatement · cited by 72
- CategoryTheory.Quotient.liftproof · cited by 11
- CategoryTheory.Localization.Construction.relationsproof · cited by 7
- CategoryTheory.Localization.Construction.liftToPathCategoryproof · cited by 4
Cited by19
Results whose statement or proof uses this declaration.
- CategoryTheory.Functor.IsLocalization.of_equivalence_targetproof · cited by 8
- CategoryTheory.Functor.IsLocalization.mk'proof · cited by 6
- CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift₁proof · cited by 4
- CategoryTheory.Localization.equivalenceFromModelproof · cited by 3
- CategoryTheory.Localization.Construction.facstatement and proof · cited by 3
- CategoryTheory.Localization.strictUniversalPropertyFixedTargetQproof · cited by 2
- CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLiftproof · cited by 2
- CategoryTheory.Functor.IsLocalization.of_equivalence_sourceproof · cited by 2
- CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₂proof · cited by 1
- CategoryTheory.Functor.IsLocalization.of_isoproof · cited by 0
- CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ_liftstatement · cited by 0