isZariskiLocalAtTarget — Mathlib

English

If P is local on both source and target and is stable under postcomposition with open immersions, then P is local on the target.

Русский

Если P локально по источнику и по цели и стабильно при посткомпозиции с открытыми вложениями, то P локально по цели.

LaTeX

$$$[P.IsMultiplicative] \; \Rightarrow \mathrm{IsZariskiLocalAtTarget} P\quad \text{assuming } P \text{ local at source and stable under open immersions}$$$

Lean4

theorem isZariskiLocalAtTarget [P.IsMultiplicative]
    (hP : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f) :
    IsZariskiLocalAtTarget P
    where
  pullbackSnd {X Y} f 𝒰 i
    hf := by
    apply hP _ (𝒰.f i)
    rw [← pullback.condition]
    exact IsZariskiLocalAtSource.comp hf _
  of_zeroHypercover {X Y} f 𝒰
    h := by
    rw [P.iff_of_zeroHypercover_source (𝒰.pullback₁ f)]
    intro i
    rw [← Scheme.Cover.pullbackHom_map]
    exact P.comp_mem _ _ (h i) (of_isOpenImmersion _)

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