English
If a property holds on all components of a source open cover after open immersions, it holds for the morphism itself.
Русский
Если свойство выполняется на всех компонентах источника по открытым покрытиям после открытых вглублениях, оно верно и для самого морфизма.
LaTeX
$$of_source_openCover$$
Lean4
theorem of_source_openCover [IsAffine Y] (𝒰 : X.OpenCover) [∀ i, IsAffine (𝒰.X i)]
(H : ∀ i, Q ((𝒰.f i ≫ f).appTop.hom)) : P f :=
by
rw [HasAffineProperty.iff_of_isAffine (P := P)]
intro U
let S i : X.affineOpens := ⟨_, isAffineOpen_opensRange (𝒰.f i)⟩
induction U using of_affine_open_cover S 𝒰.iSup_opensRange with
| basicOpen U r
H =>
simp_rw [Scheme.affineBasicOpen_coe, ← f.appLE_map (U := ⊤) le_top (homOfLE (X.basicOpen_le r)).op]
have := U.2.isLocalization_basicOpen r
exact (isLocal_ringHomProperty P).StableUnderCompositionWithLocalizationAwayTarget _ r _ H
| openCover U s hs
H =>
apply
(isLocal_ringHomProperty P).ofLocalizationSpanTarget.ofIsLocalization (isLocal_ringHomProperty P).respectsIso _ _
hs
rintro r
refine ⟨_, _, _, IsAffineOpen.isLocalization_basicOpen U.2 r, ?_⟩
rw [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, Scheme.Hom.appLE_map]
exact H r
| hU i =>
specialize H i
rw [←
(isLocal_ringHomProperty P).respectsIso.cancel_right_isIso _
((IsOpenImmersion.isoOfRangeEq (𝒰.f i) (S i).1.ι Subtype.range_coe.symm).inv.app _),
← CommRingCat.hom_comp, ← Scheme.comp_appTop, IsOpenImmersion.isoOfRangeEq_inv_fac_assoc, Scheme.comp_appTop,
Scheme.Opens.ι_appTop, Scheme.Hom.appTop, Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_map] at H
exact (f.appLE_congr _ rfl (by simp) (fun f => Q f.hom)).mp H
