English
If Q is a local property and HasAffineProperty holds, then Q.diagonal is Local.
Русский
Если Q — локальное свойство и выполняется HasAffineProperty, то диагональ Q.diagonal локальна.
LaTeX
$$Q.diagonal.IsLocal$$
Lean4
instance diagonal_affineProperty_isLocal {Q : AffineTargetMorphismProperty} [Q.IsLocal] : Q.diagonal.IsLocal
where
respectsIso := inferInstance
to_basicOpen {_ Y} _ f r
hf :=
diagonal_of_diagonal_of_isPullback (targetAffineLocally Q) (isPullback_morphismRestrict f (Y.basicOpen r)).flip
((diagonal_iff (targetAffineLocally Q)).mp hf)
of_basicOpenCover {X Y} _ f s hs
hs' := by
refine (diagonal_iff (targetAffineLocally Q)).mpr ?_
let 𝒰 := Y.openCoverOfIsOpenCover _ (((isAffineOpen_top Y).basicOpen_union_eq_self_iff _).mpr hs)
have (i : _) : IsAffine (𝒰.X i) := (isAffineOpen_top Y).basicOpen i.1
refine diagonal_of_openCover_diagonal (targetAffineLocally Q) f 𝒰 ?_
intro i
exact
(Q.diagonal.arrow_mk_iso_iff (morphismRestrictEq _ (by simp [𝒰]) ≪≫ morphismRestrictOpensRange _ _)).mp (hs' i)
