openCover — Mathlib

Lean4
/-- The open cover of the colimit of a locally directed diagram by the components. -/
@[simps! I₀ X f]
def openCover : (colimit F).OpenCover :=
  Cover.copy
    ((coverOfIsIso ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom).bind fun i ↦
      (glueData F).openCover)
    J F.obj (colimit.ι F) ((equivShrink J).trans <| (Equiv.uniqueSigma fun (_ : Unit) ↦ Shrink J).symm)
    (fun _ ↦ F.mapIso (eqToIso (by simp [GlueData.openCover, glueData]))) fun i ↦
    by
    change colimit.ι F i = _ ≫ (glueData F).ι (equivShrink J i) ≫ _
    simp [← Category.assoc, ← Iso.comp_inv_eq, cocone]
Похожие утверждения