diagonal_of_diagonal_of_isPullback

English

If iV, f', f, g form a pullback square with h a pullback, then from a diagonal property on f we obtain a diagonal property on f'.

Русский

Если iV, f', f, g образуют квадрат-подвыборку с h как диагональным, то свойство диагонали на f переходит на f'.

LaTeX

$$If IsPullback(iV, f', f, g) and H: P.diagonal f, then Q.diagonal f'.$$

Lean4

theorem diagonal_of_diagonal_of_isPullback (P) {Q} [HasAffineProperty P Q] {X Y U V : Scheme.{u}} {f : X ⟶ Y}
    {g : U ⟶ Y} [IsAffine U] [IsOpenImmersion g] {iV : V ⟶ X} {f' : V ⟶ U} (h : IsPullback iV f' f g)
    (H : P.diagonal f) : Q.diagonal f' := by
  letI := isLocal_affineProperty P
  rw [← Q.diagonal.cancel_left_of_respectsIso h.isoPullback.inv, h.isoPullback_inv_snd]
  rintro U V f₁ f₂ hU hV hf₁ hf₂
  rw [← Q.cancel_left_of_respectsIso (pullbackDiagonalMapIso f _ f₁ f₂).hom]
  convert HasAffineProperty.of_isPullback (P := P) (.of_hasPullback _ _) H
  · apply pullback.hom_ext <;> simp
  · infer_instance
  · infer_instance

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