natTransExtension — Mathlib

Lean4
/-- If `F₁` and `F₂` are functors `W.Localization ⥤ D`, a natural transformation `F₁ ⟶ F₂`
can be obtained from a natural transformation `W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂`. -/
@[simps]
def natTransExtension {F₁ F₂ : W.Localization ⥤ D} (τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂) : F₁ ⟶ F₂
    where
  app := NatTransExtension.app τ
  naturality :=
    by
    suffices MorphismProperty.naturalityProperty (NatTransExtension.app τ) = ⊤
      by
      intro X Y f
      simpa only [← this] using MorphismProperty.top_apply f
    refine
      morphismProperty_is_top' (MorphismProperty.naturalityProperty (NatTransExtension.app τ)) ?_
        (MorphismProperty.naturalityProperty.stableUnderInverse _)
    intro X Y f
    dsimp
    simpa only [NatTransExtension.app_eq] using τ.naturality f
Похожие утверждения