Theorems · Theorem · category theory

CategoryTheory.Functor.IsLocalization.comp

∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (L₁ : CategoryTheory.Functor C₁ C₂) (L₂ : CategoryTheory.Functor C₂ C₃) (W₁ : CategoryTheory.MorphismProperty C₁)
  (W₂ : CategoryTheory.MorphismProperty C₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂]
  (W₃ : CategoryTheory.MorphismProperty C₁),
  W₃.IsInvertedBy (L₁.comp L₂) → W₁ ≤ W₃ → W₂ ≤ W₃.map L₁ → (L₁.comp L₂).IsLocalization W₃

Defined in: Mathlib.CategoryTheory.Localization.Composition
Cited by: 1 results in Mathlib
Foundations: Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.Category CategoryTheory.Category CategoryTheory.Functor.IsLocalization CategoryTheory.Functor.IsLocalization

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites47

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.Functor.compstatement and proof · cited by 6,529
CategoryTheory.Isoproof · cited by 3,963
LE.le.transproof · cited by 3,151
CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
le_reflproof · cited by 2,061
CategoryTheory.Equivalence.functorproof · cited by 1,268
CategoryTheory.Equivalence.inverseproof · cited by 1,130
CategoryTheory.Iso.symmproof · cited by 993
CategoryTheory.Equivalenceproof · cited by 601
CategoryTheory.Iso.transproof · cited by 566

Cited by1

Results whose statement or proof uses this declaration.

CategoryTheory.Functor.IsLocalization.of_compproof · cited by 0