English
If a property P of ring homomorphisms is invariant under isomorphisms, then the derived property 'sourceAffineLocally P' is also invariant under isomorphisms.
Русский
Если свойство P относительно гомоморфизмов колец инвариантно под изоморфизмами, то выведенное свойство 'sourceAffineLocally P' также инвариантно под изоморфизмами.
LaTeX
$$$\\operatorname{RespectsIso}(P) \\Rightarrow \\operatorname{RespectsIso}\\big((\\mathrm{sourceAffineLocally}\\ P)\\big)$$$
Lean4
theorem sourceAffineLocally_respectsIso (h₁ : RingHom.RespectsIso P) : (sourceAffineLocally P).toProperty.RespectsIso :=
by
apply AffineTargetMorphismProperty.respectsIso_mk
· introv H U
have : IsIso (e.hom.appLE (e.hom ''ᵁ U) U.1 (e.hom.preimage_image_eq _).ge) :=
inferInstanceAs (IsIso (e.hom.app _ ≫ X.presheaf.map (eqToHom (e.hom.preimage_image_eq _).symm).op))
rw [← Scheme.appLE_comp_appLE _ _ ⊤ (e.hom ''ᵁ U) U.1 le_top (e.hom.preimage_image_eq _).ge, CommRingCat.hom_comp,
h₁.cancel_right_isIso]
exact H ⟨_, U.prop.image_of_isOpenImmersion e.hom⟩
· introv H U
rw [Scheme.comp_appLE, CommRingCat.hom_comp, h₁.cancel_left_isIso]
exact H U
