vPullbackConeIsLimitOfMap — Mathlib

English

If F preserves the gluing and reflects the pullback of the injections into glued, then the vPullbackCone is a limit cone in D.

Русский

Если F сохраняет склейку и отражает pullback инъекций в склейке, то vPullbackCone является пределом.

LaTeX

$$$\\text{vPullbackConeIsLimitOfMap}(D,F,i,j)$. IsLimit((D.mapGlueData F).vPullbackCone i j) \\Rightarrow IsLimit(D.vPullbackCone i j).$$$

Lean4

/-- If `F` preserves the gluing, and reflects the pullback of `U i ⟶ glued` and `U j ⟶ glued`,
then `F` reflects the fact that `V_pullback_cone` is a pullback. -/
def vPullbackConeIsLimitOfMap (i j : D.J) [ReflectsLimit (cospan (D.ι i) (D.ι j)) F]
    (hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)) : IsLimit (D.vPullbackCone i j) :=
  by
  apply isLimitOfReflects F
  apply (isLimitMapConePullbackConeEquiv _ _).symm _
  let e : cospan (F.map (D.ι i)) (F.map (D.ι j)) ≅ cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
    NatIso.ofComponents
      (fun x => by
        cases x
        exacts [D.gluedIso F, Iso.refl _])
      (by rintro (_ | _) (_ | _) (_ | _ | _) <;> simp)
  apply IsLimit.postcomposeHomEquiv e _ _
  apply hc.ofIsoLimit
  refine Cones.ext (Iso.refl _) ?_
  rintro (_ | _ | _)
  all_goals simp [e]; rfl

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