mk — Mathlib · SciLib

English

If P is a morphism property stable under iso and satisfies a base-change condition with respect to affines, then P is stable under base change.

Русский

Если свойство P сохраняется при изоморфизмах и удовлетворяет условию базового спуска по аффинным схожим отображениям, то оно стабильно относительно оснований.

LaTeX

$$$P.IsStableUnderBaseChange$ under the given hypotheses.$$

Lean4

theorem mk (P : AffineTargetMorphismProperty) [P.toProperty.RespectsIso]
    (H : ∀ ⦃X Y S : Scheme⦄ [IsAffine S] [IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)) :
    P.IsStableUnderBaseChange := by
  intro Z X Y S _ _ f g f' g' h hg
  rw [← P.cancel_left_of_respectsIso h.isoPullback.inv, h.isoPullback_inv_fst]
  exact H f g hg

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