affineAnd_le_affineAnd — Mathlib

English

If P isHasAffineProperty via affineAnd(Q) then P ≤ IsAffineHom.

Русский

Если P имеет свойство HasAffineProperty через affineAnd(Q), то P ⊆ IsAffineHom.

LaTeX

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

Lean4

theorem affineAnd_le_affineAnd {P P' : MorphismProperty Scheme.{u}} (hP : HasAffineProperty P (affineAnd Q))
    (hP' : HasAffineProperty P' (affineAnd Q'))
    (hQQ' : ∀ {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S}, Q f → Q' f) : P ≤ P' :=
  by
  rw [HasAffineProperty.eq_targetAffineLocally (P := P), HasAffineProperty.eq_targetAffineLocally (P := P')]
  exact targetAffineLocally_affineAnd_le hQQ'

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