openCoverOfLeft — Mathlib

Lean4
/-- Given an open cover `{ Xᵢ }` of `X`, then `X ×[Z] Y` is covered by `Xᵢ ×[Z] Y`. -/
@[simps! I₀ X f]
def openCoverOfLeft (𝒰 : OpenCover X) (f : X ⟶ Z) (g : Y ⟶ Z) : OpenCover (pullback f g) :=
  by
  fapply
    ((gluing 𝒰 f g).openCover.pushforwardIso (limit.isoLimitCone ⟨_, gluedIsLimit 𝒰 f g⟩).inv).copy 𝒰.I₀
      (fun i => pullback (𝒰.f i ≫ f) g)
      (fun i => pullback.map _ _ _ _ (𝒰.f i) (𝟙 _) (𝟙 _) (Category.comp_id _) (by simp)) (Equiv.refl 𝒰.I₀) fun _ =>
      Iso.refl _
  rintro (i : 𝒰.I₀)
  simp_rw [Cover.pushforwardIso_I₀, Cover.pushforwardIso_f, GlueData.openCover_f, GlueData.openCover_I₀, gluing_J]
  exact pullback.hom_ext (by simp [p1]) (by simp [p2])
Похожие утверждения