localizerMorphismInv

Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

URI: https://scilib.ai/kg/mathlib#CategoryTheory.LocalizerMorphism.functorialRightResolutions.localizerMorphismInv

Lean4

/-- If `Φ : LocalizerMorphism W₁ W₂` corresponds to a class `W₁` that is
the inverse image of `W₂` by the functor `Φ.functor` and that we
have functorial right resolutions, then this is a morphism of localizers
in the other direction. -/
@[simps]
def localizerMorphismInv [W₂.HasTwoOutOfThreeProperty] : LocalizerMorphism W₂ W₁
    where
  functor := ρ
  map := by
    rw [hW₁]
    intro X Y f hf
    have := i.naturality f
    dsimp at this
    simp only [MorphismProperty.inverseImage_iff]
    rw [← W₂.precomp_iff _ _ (hi X), ← this]
    exact W₂.comp_mem _ _ hf (hi Y)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru