specTargetImageFactorization_comp

English

The composition of the factorization with Spec.map equals f.

Русский

Состава факторизации с отображением Spec.map равно исходному f.

LaTeX

$$$ (\mathrm{specTargetImageFactorization} f) \; ≫ \mathrm{Spec.map}( \mathrm{specTargetImageRingHom} f) = f $$$

Lean4

@[reassoc (attr := simp)]
theorem specTargetImageFactorization_comp : specTargetImageFactorization f ≫ Spec.map (specTargetImageRingHom f) = f :=
  f.liftQuotient_comp _ _

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