English
HoldsForLocalizationAway (IsStandardSmoothOfRelativeDimension 0).
Русский
HoldsForLocalizationAway (IsStandardSmoothOfRelativeDimension 0).
LaTeX
$$$$ \operatorname{HoldsForLocalizationAway}( \operatorname{IsStandardSmoothOfRelativeDimension}(0) ). $$$$
Lean4
theorem isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway :
StableUnderCompositionWithLocalizationAway (IsStandardSmoothOfRelativeDimension n)
where
left R S _ _ _ _ _ r _ _
hf :=
have : (algebraMap R S).IsStandardSmoothOfRelativeDimension 0 :=
IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway r
add_zero n ▸ IsStandardSmoothOfRelativeDimension.comp hf this
right _ S T _ _ _ _ s _ _
hf :=
have : (algebraMap S T).IsStandardSmoothOfRelativeDimension 0 :=
IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway s
zero_add n ▸ IsStandardSmoothOfRelativeDimension.comp this hf
