English
Assume that for all ring homomorphisms f,g, if the composite g∘f has property Q then g has property Q. Then for any scheme morphisms f:X→Y and g:Y→Z, if the composition f≫g has property P, then f has property P.
Русский
Пусть для всех кольцевых гомоморфизмов f,g: если композиция g∘f имеет свойство Q, тогда свойство Q дано для g. Тогда при морфизмах схем f:X→Y, g:Y→Z: если композиция f≫g имеет свойство P, то свойство P имеет и f.
LaTeX
$$$(\forall R,S,T\ f:R\to S,\ g:S\to T,\ Q(g\circ f)\Rightarrow Q g) \Rightarrow \forall {X,Y,Z} \ f:X\to Y,\ g:Y\to Z,\ P(f\circ g) \Rightarrow P(f).$$$
Lean4
theorem of_comp
(H : ∀ {R S T : Type u} [CommRing R] [CommRing S] [CommRing T], ∀ (f : R →+* S) (g : S →+* T), Q (g.comp f) → Q g)
{X Y Z : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} (h : P (f ≫ g)) : P f :=
by
wlog hZ : IsAffine Z generalizing X Y Z
· rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (g.preimage_iSup_eq_top (iSup_affineOpens_eq_top Z))]
intro U
have H := IsZariskiLocalAtTarget.restrict h U.1
rw [morphismRestrict_comp] at H
exact this H inferInstance
wlog hY : IsAffine Y generalizing X Y
· rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top Y)]
intro U
have H := comp_of_isOpenImmersion P (f ⁻¹ᵁ U.1).ι (f ≫ g) h
rw [← morphismRestrict_ι_assoc] at H
exact this H inferInstance
wlog hY : IsAffine X generalizing X
· rw [IsZariskiLocalAtSource.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top X)]
intro U
have H := comp_of_isOpenImmersion P U.1.ι (f ≫ g) h
rw [← Category.assoc] at H
exact this H inferInstance
rw [iff_of_isAffine (P := P)] at h ⊢
exact H _ _ h
