openCoverOfBase — Mathlib

Lean4
/-- Given an open cover `{ Zᵢ }` of `Z`, then `X ×[Z] Y` is covered by `Xᵢ ×[Zᵢ] Yᵢ`, where
  `Xᵢ = X ×[Z] Zᵢ` and `Yᵢ = Y ×[Z] Zᵢ` is the preimage of `Zᵢ` in `X` and `Y`. -/
@[simps! I₀ X f]
def openCoverOfBase (𝒰 : OpenCover Z) (f : X ⟶ Z) (g : Y ⟶ Z) : OpenCover (pullback f g) :=
  by
  apply
    (openCoverOfBase'.{u, u} 𝒰 f g).copy 𝒰.I₀
      (fun i => pullback (pullback.snd _ _ : pullback f (𝒰.f i) ⟶ _) (pullback.snd _ _ : pullback g (𝒰.f i) ⟶ _))
      (fun i =>
        pullback.map _ _ _ _ (pullback.fst _ _) (pullback.fst _ _) (𝒰.f i) pullback.condition.symm
          pullback.condition.symm)
      ((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit).symm) fun _ => Iso.refl _
  intro i
  rw [Iso.refl_hom, Category.id_comp, openCoverOfBase'_f]
  ext : 1 <;>
    · simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, Equiv.trans_apply, Equiv.prodPUnit_symm_apply,
        Category.assoc, limit.lift_π_assoc, cospan_left, Category.comp_id, limit.isoLimitCone_inv_π_assoc,
        PullbackCone.π_app_left, IsPullback.cone_fst, pullbackSymmetry_hom_comp_snd_assoc, limit.isoLimitCone_inv_π,
        PullbackCone.π_app_right, IsPullback.cone_snd, pullbackSymmetry_hom_comp_fst_assoc]
      rfl
Похожие утверждения