instIsSmoothOfRelativeDimensionOfNatNatCompScheme

English

If f and g are smooth of relative dimension 0, then their composition is smooth of relative dimension 0.

Русский

Если f и g гладкие относительной размерности 0, то их композиция гладкая относительной размерности 0.

LaTeX

$$If IsSmoothOfRelativeDimension 0 f and IsSmoothOfRelativeDimension 0 g, then IsSmoothOfRelativeDimension 0 (f ≫ g)$$

Lean4

instance {Z : Scheme.{u}} (g : Y ⟶ Z) [IsSmoothOfRelativeDimension 0 f] [IsSmoothOfRelativeDimension 0 g] :
    IsSmoothOfRelativeDimension 0 (f ≫ g) :=
  inferInstanceAs <| IsSmoothOfRelativeDimension (0 + 0) (f ≫ g)

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