affineAnd_le_isAffineHom — Mathlib

English

If P is affine locally defined by affineAnd(Q) and Q holds, then P is contained in IsAffineHom.

Русский

Если P локально через affineAnd(Q) и Q выполняется, то P ⊆ IsAffineHom.

LaTeX

$$$P \\leq \\operatorname{IsAffineHom}$$$

Lean4

theorem affineAnd_le_isAffineHom (P : MorphismProperty Scheme.{u}) (hA : HasAffineProperty P (affineAnd Q)) :
    P ≤ @IsAffineHom := by
  intro X Y f hf
  wlog hY : IsAffine Y
  · rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsAffineHom) _ (iSup_affineOpens_eq_top _)]
    intro U
    exact this P hA _ (IsZariskiLocalAtTarget.restrict hf _) U.2
  rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))] at hf
  rw [HasAffineProperty.iff_of_isAffine (P := @IsAffineHom)]
  exact hf.1

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