instPreservesFiniteProductsUnderPushout

English

Let f: R → S be a ring homomorphism. If f is flat, then the Under pushout by f preserves finite products.

Русский

Пусть f: R → S — гомоморфизм колец. Если f плоский, то отображение Under.pushout f сохраняет конечные произведения.

LaTeX

$$$\\text{Flat}(f) \\Rightarrow \\mathrm{PreservesFiniteProducts}(\\mathrm{Under.pushout}(f)).$$$

Lean4

/-- `Under.pushout f` preserves finite products. -/
instance : PreservesFiniteProducts (Under.pushout f) where
  preserves
    _ :=
    letI : Algebra R S := f.hom.toAlgebra
    preservesLimitsOfShape_of_natIso (tensorProdIsoPushout R S)

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