affineAnd — Mathlib

English

For any Q respecting isomorphisms, the affine target property affineAnd Q evaluates to (IsAffine X) ∧ Q (f.appTop).hom when f targets an affine scheme.

Русский

Для любых Q, сохраняющих изоморфизмы, свойство аффинной цели affineAnd Q равно (IsAffine X) ∧ Q (f.appTop).hom, если цель - аффинна.

LaTeX

$$affineAnd Q f ↔ IsAffine X ∧ Q (f.appTop).hom$$

Lean4

/-- This is the affine target morphism property where the source is affine and
the induced map of rings on global sections satisfies `P`. -/
def affineAnd : AffineTargetMorphismProperty := fun X _ f ↦ IsAffine X ∧ Q (f.appTop).hom

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