instCompScheme — Mathlib

English

Let f: X → Y and g: Y → Z be morphisms of schemes. If f and g are finite, then the composition f ∘ g is finite.

Русский

Пусть f: X → Y и g: Y → Z — конечные морфизмы. Тогда композиция f ∘ g является конечным морфизмом.

LaTeX

$$$\text{If } f: X \to Y \text{ and } g: Y \to Z \text{ are finite morphisms, then } f \circ g \text{ is finite.}$$$

Lean4

instance {Z : Scheme.{u}} (g : Y ⟶ Z) [IsFinite f] [IsFinite g] : IsFinite (f ≫ g) :=
  IsStableUnderComposition.comp_mem f g ‹IsFinite f› ‹IsFinite g›

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