instIsStableUnderBaseChangeScheme

English

IsPreimmersion is stable under base change: if f: X → Y is a preimmersion and one forms the pullback along g: Y' → Y, then the base-changed map is also a preimmersion.

Русский

Предиммерсия сохраняется при базовом изменении: если f: X → Y — предиммersion, и взяв базовую тяготу вдоль g: Y' → Y, получившаяся база-измененная карта также является предиммерсией.

LaTeX

$$$\forall X,Y,Z\, (f: X\to Y)\, (g: Y\to Z),\; IsPreimmersion(f) \Rightarrow IsPreimmersion(\text{pullback}(f,g))$$$

Lean4

instance : IsStableUnderBaseChange @IsPreimmersion :=
  by
  refine .mk' fun X Y Z f g _ _ ↦ ?_
  have := pullback_fst (P := @SurjectiveOnStalks) f g inferInstance
  constructor
  let L (x : (pullback f g :)) : {x : X × Y | f.base x.1 = g.base x.2} :=
    ⟨⟨(pullback.fst f g).base x, (pullback.snd f g).base x⟩, by
      simp only [Set.mem_setOf, ← Scheme.comp_base_apply, pullback.condition]⟩
  have : IsEmbedding L :=
    IsEmbedding.of_comp (by fun_prop) continuous_subtype_val (SurjectiveOnStalks.isEmbedding_pullback f g)
  exact
    IsEmbedding.subtypeVal.comp ((TopCat.pullbackHomeoPreimage _ f.continuous _ g.isEmbedding).isEmbedding.comp this)

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