Properties of morphisms from properties of ring homs.

We provide the basic framework for talking about properties of morphisms that come from properties of ring homs. For P a property of ring homs, we have two ways of defining a property of scheme morphisms:

Let f : X ⟶ Y,

• targetAffineLocally (affine_and P): the preimage of an affine open U = Spec A is affine (= Spec B) and A ⟶ B satisfies P. (TODO)
• affineLocally P: For each pair of affine open U = Spec A ⊆ X and V = Spec B ⊆ f ⁻¹' U, the ring hom A ⟶ B satisfies P.

For these notions to be well defined, we require P be a sufficient local property. For the former, P should be local on the source (RingHom.RespectsIso P, RingHom.LocalizationPreserves P, RingHom.OfLocalizationSpan), and targetAffineLocally (affine_and P) will be local on the target. (TODO)

For the latter P should be local on the target (RingHom.PropertyIsLocal P), and affineLocally P will be local on both the source and the target.

Further more, these properties are stable under compositions (resp. base change) if P is. (TODO)

theorem RingHom.RespectsIso.basicOpen_iff {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.RespectsIso P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) (r : ↑(Y.presheaf.obj (Opposite.op ⊤))) : P (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict Y (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion (AlgebraicGeometry.Scheme.basicOpen Y r))))))) (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ((TopologicalSpace.Opens.map f.val.base).obj (AlgebraicGeometry.Scheme.basicOpen Y r)))))))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict Y (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion (AlgebraicGeometry.Scheme.basicOpen Y r))))))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ((TopologicalSpace.Opens.map f.val.base).obj (AlgebraicGeometry.Scheme.basicOpen Y r)))))))) (AlgebraicGeometry.Scheme.Γ.map (f ∣_ AlgebraicGeometry.Scheme.basicOpen Y r).op) ↔ P (↑(Y.presheaf.obj (Opposite.op (AlgebraicGeometry.Scheme.basicOpen Y r)))) (↑(X.presheaf.obj (Opposite.op (AlgebraicGeometry.Scheme.basicOpen X (↑(AlgebraicGeometry.Scheme.Γ.map f.op) r))))) (CommRingCat.instCommRingα (Y.presheaf.obj (Opposite.op (AlgebraicGeometry.Scheme.basicOpen Y r)))) (CommRingCat.instCommRingα (X.presheaf.obj (Opposite.op (AlgebraicGeometry.Scheme.basicOpen X (↑(AlgebraicGeometry.Scheme.Γ.map f.op) r))))) (IsLocalization.Away.map (↑(Y.presheaf.obj (Opposite.op (AlgebraicGeometry.Scheme.basicOpen Y r)))) (↑(X.presheaf.obj (Opposite.op (AlgebraicGeometry.Scheme.basicOpen X (↑(AlgebraicGeometry.Scheme.Γ.map f.op) r))))) (AlgebraicGeometry.Scheme.Γ.map f.op) r)

theorem RingHom.RespectsIso.basicOpen_iff_localization {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.RespectsIso P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) (r : ↑(Y.presheaf.obj (Opposite.op ⊤))) : P (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict Y (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion (AlgebraicGeometry.Scheme.basicOpen Y r))))))) (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ((TopologicalSpace.Opens.map f.val.base).obj (AlgebraicGeometry.Scheme.basicOpen Y r)))))))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict Y (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion (AlgebraicGeometry.Scheme.basicOpen Y r))))))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ((TopologicalSpace.Opens.map f.val.base).obj (AlgebraicGeometry.Scheme.basicOpen Y r)))))))) (AlgebraicGeometry.Scheme.Γ.map (f ∣_ AlgebraicGeometry.Scheme.basicOpen Y r).op) ↔ P (Localization.Away r) (Localization.Away (↑(AlgebraicGeometry.Scheme.Γ.map f.op) r)) Localization.instCommRingLocalizationToCommMonoid Localization.instCommRingLocalizationToCommMonoid (Localization.awayMap (AlgebraicGeometry.Scheme.Γ.map f.op) r)

theorem RingHom.RespectsIso.ofRestrict_morphismRestrict_iff {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.RespectsIso P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) (r : ↑(Y.presheaf.obj (Opposite.op ⊤))) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hU : AlgebraicGeometry.IsAffineOpen U) {V : TopologicalSpace.Opens ↑↑(AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ((TopologicalSpace.Opens.map f.val.base).obj (AlgebraicGeometry.Scheme.basicOpen Y r))))).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace} (e : V = (TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.ofRestrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ((TopologicalSpace.Opens.map f.val.base).obj (AlgebraicGeometry.Scheme.basicOpen Y r))))).val.base).obj U) : P (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict Y (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion (AlgebraicGeometry.Scheme.basicOpen Y r))))))) (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ((TopologicalSpace.Opens.map f.val.base).obj (AlgebraicGeometry.Scheme.basicOpen Y r))))) (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion V)))))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict Y (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion (AlgebraicGeometry.Scheme.basicOpen Y r))))))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ((TopologicalSpace.Opens.map f.val.base).obj (AlgebraicGeometry.Scheme.basicOpen Y r))))) (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion V)))))) (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ofRestrict (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ((TopologicalSpace.Opens.map f.val.base).obj (AlgebraicGeometry.Scheme.basicOpen Y r))))) (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion V))) (f ∣_ AlgebraicGeometry.Scheme.basicOpen Y r)).op) ↔ P (Localization.Away r) (Localization.Away (↑(AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ofRestrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion U))) f).op) r)) Localization.instCommRingLocalizationToCommMonoid Localization.instCommRingLocalizationToCommMonoid (Localization.awayMap (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ofRestrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion U))) f).op) r)

theorem RingHom.StableUnderBaseChange.Γ_pullback_fst {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.StableUnderBaseChange P) (hP' : RingHom.RespectsIso P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] [AlgebraicGeometry.IsAffine S] (f : X ⟶ S) (g : Y ⟶ S) (H : P (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op S))) (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op Y))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op S))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op Y))) (AlgebraicGeometry.Scheme.Γ.map g.op)) : P (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op X))) (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (CategoryTheory.Limits.pullback f g)))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op X))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (CategoryTheory.Limits.pullback f g)))) (AlgebraicGeometry.Scheme.Γ.map CategoryTheory.Limits.pullback.fst.op)

def AlgebraicGeometry.sourceAffineLocally (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : AlgebraicGeometry.AffineTargetMorphismProperty

For P a property of ring homomorphisms, sourceAffineLocally P holds for f : X ⟶ Y whenever P holds for the restriction of f on every affine open subset of X.

@[inline, reducible]

abbrev AlgebraicGeometry.affineLocally (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme

For P a property of ring homomorphisms, affineLocally P holds for f : X ⟶ Y if for each affine open U = Spec A ⊆ Y and V = Spec B ⊆ f ⁻¹' U, the ring hom A ⟶ B satisfies P. Also see affineLocally_iff_affineOpens_le.

theorem AlgebraicGeometry.sourceAffineLocally_respectsIso {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (h₁ : RingHom.RespectsIso P) : CategoryTheory.MorphismProperty.RespectsIso (AlgebraicGeometry.AffineTargetMorphismProperty.toProperty (AlgebraicGeometry.sourceAffineLocally P))

theorem AlgebraicGeometry.affineLocally_respectsIso {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (h : RingHom.RespectsIso P) : CategoryTheory.MorphismProperty.RespectsIso (AlgebraicGeometry.affineLocally P)

theorem AlgebraicGeometry.affineLocally_iff_affineOpens_le {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.RespectsIso P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.affineLocally P f ↔ (U : ↑(AlgebraicGeometry.Scheme.affineOpens Y)) → (V : ↑(AlgebraicGeometry.Scheme.affineOpens X)) → (e : ↑V ≤ (TopologicalSpace.Opens.map f.val.base).obj ↑U) → P (↑(Y.presheaf.obj (Opposite.op ↑U))) (↑(X.presheaf.obj (Opposite.op ↑V))) (CommRingCat.instCommRingα (Y.presheaf.obj (Opposite.op ↑U))) (CommRingCat.instCommRingα (X.presheaf.obj (Opposite.op ↑V))) (AlgebraicGeometry.Scheme.Hom.appLe f e)

theorem AlgebraicGeometry.scheme_restrict_basicOpen_of_localizationPreserves {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (h₁ : RingHom.RespectsIso P) (h₂ : RingHom.LocalizationPreserves P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) (r : ↑(Y.presheaf.obj (Opposite.op ⊤))) (H : AlgebraicGeometry.sourceAffineLocally P f) (U : ↑(AlgebraicGeometry.Scheme.affineOpens (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ((TopologicalSpace.Opens.map f.val.base).obj (AlgebraicGeometry.Scheme.basicOpen Y r))))))) : P (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict Y (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion (AlgebraicGeometry.Scheme.basicOpen Y r))))))) (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ((TopologicalSpace.Opens.map f.val.base).obj (AlgebraicGeometry.Scheme.basicOpen Y r))))) (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ↑U)))))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict Y (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion (AlgebraicGeometry.Scheme.basicOpen Y r))))))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ((TopologicalSpace.Opens.map f.val.base).obj (AlgebraicGeometry.Scheme.basicOpen Y r))))) (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ↑U)))))) (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ofRestrict (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ((TopologicalSpace.Opens.map f.val.base).obj (AlgebraicGeometry.Scheme.basicOpen Y r))))) (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ↑U))) (f ∣_ AlgebraicGeometry.Scheme.basicOpen Y r)).op)

theorem AlgebraicGeometry.sourceAffineLocally_isLocal {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (h₁ : RingHom.RespectsIso P) (h₂ : RingHom.LocalizationPreserves P) (h₃ : RingHom.OfLocalizationSpan P) : AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal (AlgebraicGeometry.sourceAffineLocally P)

theorem AlgebraicGeometry.sourceAffineLocally_of_source_open_cover_aux {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (h₁ : RingHom.RespectsIso P) (h₃ : RingHom.OfLocalizationSpanTarget P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : ↑(AlgebraicGeometry.Scheme.affineOpens X)) (s : Set ↑(X.presheaf.obj (Opposite.op ↑U))) (hs : Ideal.span s = ⊤) (hs' : (r : ↑s) → P (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op Y))) (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion (AlgebraicGeometry.Scheme.basicOpen X ↑r))))))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op Y))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion (AlgebraicGeometry.Scheme.basicOpen X ↑r))))))) (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ofRestrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion (AlgebraicGeometry.Scheme.basicOpen X ↑r)))) f).op)) : P (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op Y))) (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ↑U)))))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op Y))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ↑U)))))) (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ofRestrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ↑U))) f).op)

theorem AlgebraicGeometry.isOpenImmersionCat_comp_of_sourceAffineLocally {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (h₁ : RingHom.RespectsIso P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Z] (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (g : Y ⟶ Z) (h₂ : AlgebraicGeometry.sourceAffineLocally P g) : P (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op Z))) (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op X))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op Z))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op X))) (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp f g).op)

theorem RingHom.PropertyIsLocal.sourceAffineLocally_of_source_openCover {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.PropertyIsLocal P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffine Y] (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)] (H : (i : 𝒰.J) → P (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op Y))) (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op Y))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)))) (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f).op)) : AlgebraicGeometry.sourceAffineLocally P f

theorem RingHom.PropertyIsLocal.affine_openCover_TFAE {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.PropertyIsLocal P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) : List.TFAE [AlgebraicGeometry.sourceAffineLocally P f, ∃ 𝒰 x, (i : 𝒰.J) → P (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op Y))) (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op Y))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)))) (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f).op), (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) → [inst : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)] → (i : 𝒰.J) → P (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op Y))) (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op Y))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)))) (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f).op), {U : AlgebraicGeometry.Scheme} → (g : U ⟶ X) → [inst : AlgebraicGeometry.IsAffine U] → [inst : AlgebraicGeometry.IsOpenImmersion g] → P (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op Y))) (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op U))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op Y))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op U))) (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp g f).op)]

theorem RingHom.PropertyIsLocal.openCover_TFAE {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.PropertyIsLocal P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) : List.TFAE [AlgebraicGeometry.sourceAffineLocally P f, ∃ 𝒰, ∀ (i : 𝒰.J), AlgebraicGeometry.sourceAffineLocally P (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f), ∀ (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (i : 𝒰.J), AlgebraicGeometry.sourceAffineLocally P (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f), ∀ {U : AlgebraicGeometry.Scheme} (g : U ⟶ X) [inst : AlgebraicGeometry.IsOpenImmersion g], AlgebraicGeometry.sourceAffineLocally P (CategoryTheory.CategoryStruct.comp g f)]

theorem RingHom.PropertyIsLocal.sourceAffineLocally_comp_of_isOpenImmersion {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.PropertyIsLocal P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Z] (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsOpenImmersion f] (H : AlgebraicGeometry.sourceAffineLocally P g) : AlgebraicGeometry.sourceAffineLocally P (CategoryTheory.CategoryStruct.comp f g)

theorem RingHom.PropertyIsLocal.source_affine_openCover_iff {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.PropertyIsLocal P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffine Y] (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)] : AlgebraicGeometry.sourceAffineLocally P f ↔ (i : 𝒰.J) → P (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op Y))) (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op Y))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)))) (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f).op)

theorem RingHom.PropertyIsLocal.isLocal_sourceAffineLocally {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.PropertyIsLocal P) : AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal (AlgebraicGeometry.sourceAffineLocally P)

theorem RingHom.PropertyIsLocal.is_local_affineLocally {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.PropertyIsLocal P) : AlgebraicGeometry.PropertyIsLocalAtTarget (AlgebraicGeometry.affineLocally P)

theorem RingHom.PropertyIsLocal.affine_openCover_iff {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.PropertyIsLocal P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)] (𝒰' : (i : (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f).J) → AlgebraicGeometry.Scheme.OpenCover (AlgebraicGeometry.Scheme.OpenCover.obj (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f) i)) [∀ (i : (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f).J) (j : (𝒰' i).J), AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.OpenCover.obj (𝒰' i) j)] : AlgebraicGeometry.affineLocally P f ↔ (i : (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f).J) → (j : (𝒰' i).J) → P (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)))) (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.OpenCover.obj (𝒰' i) j)))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)))) (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.OpenCover.obj (𝒰' i) j)))) (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map (𝒰' i) j) CategoryTheory.Limits.pullback.snd).op)

theorem RingHom.PropertyIsLocal.source_openCover_iff {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.PropertyIsLocal P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) : AlgebraicGeometry.affineLocally P f ↔ (i : 𝒰.J) → AlgebraicGeometry.affineLocally P (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f)

theorem RingHom.PropertyIsLocal.affineLocally_of_isOpenImmersion {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.PropertyIsLocal P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [hf : AlgebraicGeometry.IsOpenImmersion f] : AlgebraicGeometry.affineLocally P f

theorem RingHom.PropertyIsLocal.affineLocally_of_comp {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.PropertyIsLocal P) (H : {R S T : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : CommRing T] → (f : R →+* S) → (g : S →+* T) → P R T inst inst_2 (RingHom.comp g f) → P S T inst_1 inst_2 g) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {g : Y ⟶ Z} (h : AlgebraicGeometry.affineLocally P (CategoryTheory.CategoryStruct.comp f g)) : AlgebraicGeometry.affineLocally P f

theorem RingHom.PropertyIsLocal.affineLocally_stableUnderComposition {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.PropertyIsLocal P) : CategoryTheory.MorphismProperty.StableUnderComposition (AlgebraicGeometry.affineLocally P)