instIsMultiplicativeScheme — Mathlib

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

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