English
If a property P is affine locally defined by affineAnd(Q) and Q is stable under composition, then P is stable under composition.
Русский
Если свойство P задаётся локально через affineAnd(Q) и Q устойчиво к композиции, то и P устойчиво к композиции.
LaTeX
$$$P\\text{ IsStableUnderComposition}$ under the above assumptions$$
Lean4
/-- If `P` is a morphism property affine locally defined by `affineAnd Q`, `P` is stable under
composition if `Q` is. -/
theorem affineAnd_isStableUnderComposition {P : MorphismProperty Scheme.{u}} (hA : HasAffineProperty P (affineAnd Q))
(hQ : RingHom.StableUnderComposition Q) : P.IsStableUnderComposition where
comp_mem {X Y Z} f g hf
hg := by
wlog hZ : IsAffine Z
· rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]
intro U
rw [morphismRestrict_comp]
exact this hA hQ _ _ (IsZariskiLocalAtTarget.restrict hf _) (IsZariskiLocalAtTarget.restrict hg _) U.2
rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))] at hg
obtain ⟨hY, hg⟩ := hg
rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))] at hf
obtain ⟨hX, hf⟩ := hf
rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))]
exact ⟨hX, hQ _ _ hg hf⟩
