instIsStableUnderCompositionSchemeIsSmooth

English

If IsSmoothOfRelativeDimension n f holds, then f is smooth.

Русский

Если существует гладкость относительно размерности n, то морфизм гладок.

LaTeX

$$IsSmooth f$$

Lean4

/-- Being smooth is stable under composition. -/
instance : MorphismProperty.IsStableUnderComposition @IsSmooth :=
  HasRingHomProperty.stableUnderComposition <|
    locally_stableUnderComposition isStandardSmooth_respectsIso isStandardSmooth_localizationPreserves
      isStandardSmooth_stableUnderComposition

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