final_map — Mathlib

English

StructuredArrow.map is final if the functor T is final and its domain is filtered.

Русский

StructuredArrow.map финален, если T финален и область определения T фильтрована.

LaTeX

$$∧[IsFiltered(C)] ∧ [T.Final] ⇒ Final (StructuredArrow.map (f))$$

Lean4

/-- `StructuredArrow.map` is final if the functor `T` is final` and its domain is filtered. -/
instance final_map [IsFiltered C] {S S' : D} (f : S ⟶ S') (T : C ⥤ D) [T.Final] : Final (map (T := T) f) :=
  by
  haveI := NatIso.isIso_of_isIso_app (𝟙 T)
  have : (map₂ (F := 𝟭 C) (G := 𝟭 D) f (𝟙 T)).Final := by
    apply StructuredArrow.final_map₂_id (S := 𝟭 D) (T := T) (T' := T) f (𝟙 T)
  apply final_of_natIso (mapIsoMap₂ f).symm

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