affineAnd_isLocal_of_propertyIsLocal

English

If Q is a local property of ring homomorphisms, then affineAnd(Q) is a local morphism property as well.

Русский

Если Q — локальное свойство гомоморфизмов колец, то affineAnd(Q) также локально по структуре морфизмов.

LaTeX

$$$\\operatorname{IsLocal}(\\operatorname{affineAnd}(Q))$$$

Lean4

theorem affineAnd_isLocal_of_propertyIsLocal (hPi : RingHom.PropertyIsLocal Q) : (affineAnd Q).IsLocal :=
  affineAnd_isLocal hPi.respectsIso hPi.localizationAwayPreserves hPi.ofLocalizationSpan

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