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)