isStableUnderBaseChange — Mathlib

English

If f is an immersion, then coborderRange f → Y is dominant.

Русский

Если f — вложение, то coborderRange f → Y доминирует.

LaTeX

$$$\\text{IsDominant}(\\text{coborderRange}(f).\\ι)$$$

Lean4

instance isStableUnderBaseChange : MorphismProperty.IsStableUnderBaseChange @IsImmersion where
  of_isPullback := by
    intro X Y Y' S f g f' g' H hg
    let Z := Limits.pullback f g.coborderRange.ι
    let e : Y' ⟶ Z := Limits.pullback.lift g' (f' ≫ g.liftCoborder) (by simpa using H.w.symm)
    have : IsClosedImmersion e :=
      by
      have :=
        (IsPullback.paste_horiz_iff (.of_hasPullback f g.coborderRange.ι)
              (show e ≫ Limits.pullback.snd _ _ = _ from Limits.pullback.lift_snd _ _ _)).mp
          ?_
      · exact MorphismProperty.of_isPullback this.flip inferInstance
      · simpa [e] using H.flip
    rw [← Limits.pullback.lift_fst (f := f) (g := g.coborderRange.ι) g' (f' ≫ g.liftCoborder) (by simpa using H.w.symm)]
    infer_instance

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