targetAffineLocally_affineAnd_eq_affineLocally

English

The targetAffineLocally affineAnd(Q) equals the conjunction IsAffineHom ∧ affineLocally(Q).

Русский

Целевое локальноe affineAnd(Q) равняется конъюнкции IsAffineHom и affineLocally(Q).

LaTeX

$$$\\operatorname{targetAffineLocally}(\\operatorname{affineAnd}(Q)) = \\bigl(\\operatorname{IsAffineHom} \\;\\cap\\; \\operatorname{affineLocally}(Q)\\bigr)$$$

Lean4

theorem targetAffineLocally_affineAnd_eq_affineLocally (hQ : RingHom.PropertyIsLocal Q) :
    targetAffineLocally (affineAnd Q) = (@IsAffineHom ⊓ @affineLocally Q : MorphismProperty Scheme.{u}) :=
  by
  ext X Y f
  exact targetAffineLocally_affineAnd_iff_affineLocally hQ f

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