affineAnd_eq_of_propertyIsLocal — Mathlib

English

The local target condition for affineAnd(Q) is equivalent to IsAffineHom and the affineLocally condition for Q.

Русский

Условие локального соответствия цели для affineAnd(Q) эквивально IsAffineHom и локальности affineLocally для Q.

LaTeX

$$$\\operatorname{targetAffineLocally}(\\operatorname{affineAnd}(Q)) f \\iff \\operatorname{IsAffineHom}(f) \\land \\operatorname{affineLocally}(Q) f$$$

Lean4

theorem affineAnd_eq_of_propertyIsLocal {P P' : MorphismProperty Scheme.{u}} (hP : HasAffineProperty P (affineAnd Q))
    [HasRingHomProperty P' Q] : P = (@IsAffineHom ⊓ P' : MorphismProperty Scheme.{u}) :=
  by
  rw [HasAffineProperty.eq_targetAffineLocally (P := P), targetAffineLocally_affineAnd_eq_affineLocally,
    HasRingHomProperty.eq_affineLocally (P := P')]
  exact HasRingHomProperty.isLocal_ringHomProperty P'

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