instIsZariskiLocalAtTarget — Mathlib

English

The diagonal morphism pullback.diagonal f is always an immersion.

Русский

Диагональная карта pullback.diagonal f всегда является вложением.

LaTeX

$$$\\text{IsImmersion}(\\text{pullback.diagonal}(f))$$$

Lean4

instance : IsZariskiLocalAtTarget @IsImmersion :=
  by
  suffices IsZariskiLocalAtTarget (topologically fun {X Y} _ _ f ↦ IsLocallyClosed (Set.range f)) from
    isImmersion_eq_inf ▸ inferInstance
  apply (config := { allowSynthFailures := true }) topologically_isZariskiLocalAtTarget'
  · refine { precomp := ?_, postcomp := ?_ }
    · intro X Y Z i hi f hf
      change IsIso i at hi
      change IsLocallyClosed _
      simpa only [Scheme.comp_coeBase, TopCat.coe_comp, Set.range_comp, Set.range_eq_univ.mpr i.surjective,
        Set.image_univ]
    · intro X Y Z i hi f hf
      change IsIso i at hi
      change IsLocallyClosed _
      simp only [Scheme.comp_coeBase, TopCat.coe_comp, Set.range_comp]
      refine hf.image i.homeomorph.isInducing ?_
      rw [Set.range_eq_univ.mpr i.surjective]
      exact isOpen_univ.isLocallyClosed
  · simp_rw [Set.range_restrictPreimage]
    exact fun _ _ _ hU _ ↦ hU.isLocallyClosed_iff_coe_preimage

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