comp — Mathlib

English

If F and G are RepresentablyFlat, then their composition is RepresentablyFlat.

Русский

Если F и G представимо плоские, то их композиция RepresentablyFlat.

LaTeX

$$$$ \\mathrm{RepresentablyFlat}(F) \\land \\mathrm{RepresentablyFlat}(G) \\Rightarrow \\mathrm{RepresentablyFlat}(F \\circ G). $$$$

Lean4

instance comp (G : D ⥤ E) [RepresentablyFlat F] [RepresentablyFlat G] : RepresentablyFlat (F ⋙ G) :=
  by
  refine ⟨fun X => IsCofiltered.of_cone_nonempty.{0} _ (fun {J} _ _ H => ?_)⟩
  obtain ⟨c₁⟩ := IsCofiltered.cone_nonempty (H ⋙ StructuredArrow.pre X F G)
  let H₂ : J ⥤ StructuredArrow c₁.pt.right F :=
    { obj := fun j => StructuredArrow.mk (c₁.π.app j).right
      map := fun {j j'} f => StructuredArrow.homMk (H.map f).right (congrArg CommaMorphism.right (c₁.w f)) }
  obtain ⟨c₂⟩ := IsCofiltered.cone_nonempty H₂
  simp only [H₂] at c₂
  exact
    ⟨⟨StructuredArrow.mk (c₁.pt.hom ≫ G.map c₂.pt.hom),
        ⟨fun j => StructuredArrow.homMk (c₂.π.app j).right (by simp [← G.map_comp]), fun j j' f => by
          simpa using (c₂.w f).symm⟩⟩⟩

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