stableUnderComposition — Mathlib

English

Let Q be a property of ring homomorphisms that is stable under composition in the sense that if Q holds for g∘f, then Q holds for g. Then the associated scheme-morphism property P is stable under composition: if P holds for f and for g, then P holds for the composition f ≫ g.

Русский

Пусть Q — свойство гомоморфизмов колм, устойчивое к композиторам в смысле: если Q выполняется для g∘f, то Q выполняется для g. Тогда соответствующее свойство морфизмов схем P устойчиво по композиции: если P выполняется для f и для g, то P выполняется для композиции f ≫ g.

LaTeX

$$$(\forall R,S,T\ [\text{CommRing} R][\text{CommRing} S][\text{CommRing} T],\; f:R\to S\ ,\ g:S\to T,\; Q(g\circ f)\Rightarrow Q g)\;\Rightarrow\; \big(P(f)\land P(g)\big) \Rightarrow P(f\circ g).$$$

Lean4

theorem stableUnderComposition (hP : RingHom.StableUnderComposition Q) : P.IsStableUnderComposition where
  comp_mem {X Y Z} f g hf
    hg := by
    wlog hZ : IsAffine Z generalizing X Y Z
    · rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]
      intro U
      rw [morphismRestrict_comp]
      exact this _ _ (IsZariskiLocalAtTarget.restrict hf _) (IsZariskiLocalAtTarget.restrict hg _) U.2
    wlog hY : IsAffine Y generalizing X Y
    · rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) (Y.affineCover.pullback₁ f)]
      intro i
      rw [← Scheme.Cover.pullbackHom_map_assoc]
      exact
        this _ _ (IsZariskiLocalAtTarget.of_isPullback (.of_hasPullback _ _) hf) (comp_of_isOpenImmersion _ _ _ hg)
          inferInstance
    wlog hX : IsAffine X generalizing X
    · rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) X.affineCover]
      intro i
      rw [← Category.assoc]
      exact this _ (comp_of_isOpenImmersion _ _ _ hf) inferInstance
    rw [iff_of_isAffine (P := P)] at hf hg ⊢
    exact hP _ _ hg hf

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