le_of_isZariskiLocalAtSource — Mathlib

English

IsLocalIso is below every source-Zariski-local property containing identities.

Русский

IsLocalIso лежит ниже каждого свойства, локального по источнику в Зариy, содержающего тождества.

LaTeX

$$$ \forall P, (P.ContainsIdentities \land IsZariskiLocalAtSource P) \Rightarrow IsLocalIso \le P $$$

Lean4

/-- `IsLocalIso` is weaker than every source-Zariski-local property containing identities. -/
theorem le_of_isZariskiLocalAtSource (P : MorphismProperty Scheme.{u}) [P.ContainsIdentities]
    [IsZariskiLocalAtSource P] : @IsLocalIso ≤ P := by
  intro X Y f hf
  obtain ⟨𝒰, h⟩ := eq_sourceLocalClosure_isOpenImmersion ▸ hf
  rw [IsZariskiLocalAtSource.iff_of_openCover 𝒰 (P := P)]
  exact fun _ ↦ IsZariskiLocalAtSource.of_isOpenImmersion _

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