English
If Y is affine and Q.diagonal and P.diagonal are defined, then Q.diagonal f holds iff P.diagonal f holds.
Русский
Если цель Y аффина и заданы диагональ Q.diagonal и P.diagonal, то выполнение Q.diagonal f эквивалентно P.diagonal f.
LaTeX
$$Q.diagonal f \iff P.diagonal f$$
Lean4
theorem diagonal_iff (P) {Q} [HasAffineProperty P Q] {X Y} {f : X ⟶ Y} [IsAffine Y] : Q.diagonal f ↔ P.diagonal f :=
by
letI := isLocal_affineProperty P
refine ⟨fun hf ↦ ?_, diagonal_of_diagonal_of_isPullback P .of_id_fst⟩
rw [← Q.diagonal.cancel_left_of_respectsIso (pullback.fst (f := f) (g := 𝟙 Y)), pullback.condition,
Category.comp_id] at hf
let 𝒰 := X.affineCover.pushforwardIso (inv (pullback.fst (f := f) (g := 𝟙 Y)))
have (i : _) : IsAffine (𝒰.X i) := by dsimp [𝒰]; infer_instance
exact HasAffineProperty.diagonal_of_openCover P f (Scheme.coverOfIsIso (𝟙 _)) (fun _ ↦ 𝒰) (fun _ _ _ ↦ hf _ _)
