English
The class of immersions is closed under composition; i.e. if f and g are immersions, then f ≫ g is an immersion.
Русский
Класс вложений замкнут относительно композиции: если f и g — вложения, то f ≫ g — вложение.
LaTeX
$$$\\text{IsImmersion}(f) \\wedge \\text{IsImmersion}(g) \\Rightarrow \\text{IsImmersion}(f \\circ g)$$$
Lean4
instance : MorphismProperty.IsMultiplicative @IsImmersion
where
id_mem _ := inferInstance
comp_mem {X Y Z} f g hf
hg := by
refine { __ := inferInstanceAs (IsPreimmersion (f ≫ g)), isLocallyClosed_range := ?_ }
simp only [Scheme.comp_coeBase, TopCat.coe_comp, Set.range_comp]
exact f.isLocallyClosed_range.image g.isEmbedding.isInducing g.isLocallyClosed_range