affineAnd_isStableUnderBaseChange

English

If Q is stable under base change, then affineAnd(Q) is stable under base change as a morphism property.

Русский

Если Q сохраняется при базовом изменении, то affineAnd(Q) сохраняется при базовом изменении как свойство морфизма.

LaTeX

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

Lean4

/-- If `P` is stable under base change, so is `affineAnd P`. -/
theorem affineAnd_isStableUnderBaseChange (hQi : RingHom.RespectsIso Q) (hQb : RingHom.IsStableUnderBaseChange Q) :
    (affineAnd Q).IsStableUnderBaseChange :=
  by
  haveI : (affineAnd Q).toProperty.RespectsIso := affineAnd_respectsIso hQi
  apply AffineTargetMorphismProperty.IsStableUnderBaseChange.mk
  intro X Y S _ _ f g ⟨hY, hg⟩
  exact ⟨inferInstance, hQb.pullback_fst_appTop _ hQi f _ hg⟩

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