of_iso — Mathlib

English

If F is RepresentablyFlat and α: F ≅ G, then G is RepresentablyFlat.

Русский

Если F RepresentablyFlat и есть изоморфизм α: F ≅ G, тогда G RepresentablyFlat.

LaTeX

$$$$ [\\mathrm{RepresentablyFlat}(F)] \\Rightarrow [\\alpha: F \\cong G] \\Rightarrow \\mathrm{RepresentablyFlat}(G). $$$$

Lean4

/-- Being a representably flat functor is closed under natural isomorphisms. -/
theorem of_iso [RepresentablyFlat F] {G : C ⥤ D} (α : F ≅ G) : RepresentablyFlat G where
  cofiltered _ := IsCofiltered.of_equivalence (StructuredArrow.mapNatIso α)

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