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 (affineAnd P): the preimage of an affine open U = Spec A is affine (= Spec B) and A ⟶ B satisfies P. (in Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean)
• 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.

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. We also provide the following interface:

HasRingHomProperty

HasRingHomProperty P Q is a type class asserting that P is local at the target and the source, and for f : Spec B ⟶ Spec A, it is equivalent to the ring hom property Q on Γ(f).

For HasRingHomProperty P Q and f : X ⟶ Y, we provide these API lemmas:

• AlgebraicGeometry.HasRingHomProperty.iff_appLE: P f if and only if Q (f.appLE U V _) for all affine U : Opens Y and V : Opens X.
• AlgebraicGeometry.HasRingHomProperty.iff_of_source_openCover: If Y is affine, P f ↔ ∀ i, Q ((𝒰.map i ≫ f).app ⊤) for an affine open cover 𝒰 of X.
• AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine: If X and Y are affine, then P f ↔ Q (f.app ⊤).
• AlgebraicGeometry.HasRingHomProperty.Spec_iff: P (Spec.map φ) ↔ Q φ
• AlgebraicGeometry.HasRingHomProperty.iff_of_iSup_eq_top: If Y is affine, P f ↔ ∀ i, Q (f.appLE ⊤ (U i) _) for a family U of affine opens of X.
• AlgebraicGeometry.HasRingHomProperty.of_isOpenImmersion: If f is an open immersion then P f.
• AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChange: If Q is stable under base change, then so is P.

We also provide the instances P.IsMultiplicative, P.IsStableUnderComposition, IsLocalAtTarget P, IsLocalAtSource P.

theorem RingHom.IsStableUnderBaseChange.pullback_fst_app_top (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) (hP : RingHom.IsStableUnderBaseChange fun {R S : Type u} [CommRing R] [CommRing S] => P) (hP' : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) {X Y S : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] [AlgebraicGeometry.IsAffine S] (f : X ⟶ S) (g : Y ⟶ S) (H : P (AlgebraicGeometry.Scheme.Hom.app g ⊤)) : P (AlgebraicGeometry.Scheme.Hom.app (CategoryTheory.Limits.pullback.fst f g) ⊤)

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.

Equations

• AlgebraicGeometry.sourceAffineLocally P f = ∀ (U : ↑X.affineOpens), P (AlgebraicGeometry.Scheme.Hom.appLE f ⊤ ↑U ⋯)

@[reducible, inline]

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.

Equations

• AlgebraicGeometry.affineLocally P = AlgebraicGeometry.targetAffineLocally (AlgebraicGeometry.sourceAffineLocally fun {R S : Type ?u.25} [CommRing R] [CommRing S] => P)

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

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

theorem AlgebraicGeometry.sourceAffineLocally_morphismRestrict (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (hU : AlgebraicGeometry.IsAffineOpen U) : AlgebraicGeometry.sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] => P) (f ∣_ U) ↔ ∀ (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj U), P (AlgebraicGeometry.Scheme.Hom.appLE f U (↑V) e)

theorem AlgebraicGeometry.affineLocally_iff_affineOpens_le (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] => P) f ↔ ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U), P (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)

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

theorem AlgebraicGeometry.exists_basicOpen_le_appLE_of_appLE_of_isAffine {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (hPa : RingHom.StableUnderCompositionWithLocalizationAwayTarget fun {R S : Type u} [CommRing R] [CommRing S] => P) (hPl : RingHom.LocalizationAwayPreserves fun {R S : Type u} [CommRing R] [CommRing S] => P) (x : ↑↑X.toPresheafedSpace) (U₁ U₂ : ↑Y.affineOpens) (V₁ V₂ : ↑X.affineOpens) (hx₁ : x ∈ ↑V₁) (hx₂ : x ∈ ↑V₂) (e₂ : ↑V₂ ≤ (TopologicalSpace.Opens.map f.base).obj ↑U₂) (h₂ : P (AlgebraicGeometry.Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) (hfx₁ : f.base x ∈ ↑U₁) : ∃ (r : ↑(Y.presheaf.obj (Opposite.op ↑U₁))) (s : ↑(X.presheaf.obj (Opposite.op ↑V₁))) (_ : x ∈ X.basicOpen s) (e : X.basicOpen s ≤ (TopologicalSpace.Opens.map f.base).obj (Y.basicOpen r)), P (AlgebraicGeometry.Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e)

If P holds for f over affine opens U₂ of Y and V₂ of X and U₁ (resp. V₁) are open affine neighborhoods of x (resp. f.base x), then P also holds for f over some basic open of U₁ (resp. V₁).

theorem AlgebraicGeometry.exists_affineOpens_le_appLE_of_appLE {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (hPa : RingHom.StableUnderCompositionWithLocalizationAwayTarget fun {R S : Type u} [CommRing R] [CommRing S] => P) (hPl : RingHom.LocalizationAwayPreserves fun {R S : Type u} [CommRing R] [CommRing S] => P) (x : ↑↑X.toPresheafedSpace) (U₁ : Y.Opens) (U₂ : ↑Y.affineOpens) (V₁ : X.Opens) (V₂ : ↑X.affineOpens) (hx₁ : x ∈ V₁) (hx₂ : x ∈ ↑V₂) (e₂ : ↑V₂ ≤ (TopologicalSpace.Opens.map f.base).obj ↑U₂) (h₂ : P (AlgebraicGeometry.Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) (hfx₁ : f.base x ∈ U₁.carrier) : ∃ (U' : ↑Y.affineOpens) (V' : ↑X.affineOpens) (_ : ↑U' ≤ U₁) (_ : ↑V' ≤ V₁) (_ : x ∈ ↑V') (e : ↑V' ≤ (TopologicalSpace.Opens.map f.base).obj ↑U'), P (AlgebraicGeometry.Scheme.Hom.appLE f (↑U') (↑V') e)

If P holds for f over affine opens U₂ of Y and V₂ of X and U₁ (resp. V₁) are open neighborhoods of x (resp. f.base x), then P also holds for f over some affine open U' of Y (resp. V' of X) that is contained in U₁ (resp. V₁).

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

HasRingHomProperty P Q is a type class asserting that P is local at the target and the source, and for f : Spec B ⟶ Spec A, it is equivalent to the ring hom property Q. To make the proofs easier, we state it instead as

1. Q is local (See RingHom.PropertyIsLocal)
2. P f if and only if Q holds for every Γ(Y, U) ⟶ Γ(X, V) for all affine U, V. See HasRingHomProperty.iff_appLE.

• isLocal_ringHomProperty : RingHom.PropertyIsLocal fun {R S : Type u} [CommRing R] [CommRing S] => Q
• eq_affineLocally' : P = AlgebraicGeometry.affineLocally fun {R S : Type u} [CommRing R] [CommRing S] => Q

theorem AlgebraicGeometry.HasRingHomProperty.copy (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] {P' : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (e : P = P') (e' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Q' f) : AlgebraicGeometry.HasRingHomProperty P' fun {R S : Type u} [CommRing R] [CommRing S] => Q'

theorem AlgebraicGeometry.HasRingHomProperty.eq_affineLocally (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] : P = AlgebraicGeometry.affineLocally fun {R S : Type u} [CommRing R] [CommRing S] => Q

theorem AlgebraicGeometry.HasRingHomProperty.HasAffineProperty (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] : AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] => Q)

@[instance 900]

instance AlgebraicGeometry.HasRingHomProperty.instIsLocalAtTarget (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] : AlgebraicGeometry.IsLocalAtTarget P

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.HasRingHomProperty.appLE (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (H : P f) (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U) : Q (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)

theorem AlgebraicGeometry.HasRingHomProperty.app_top (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (H : P f) [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] : Q (AlgebraicGeometry.Scheme.Hom.app f ⊤)

theorem AlgebraicGeometry.HasRingHomProperty.comp_of_isOpenImmersion (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsOpenImmersion f] (H : P g) : P (CategoryTheory.CategoryStruct.comp f g)

theorem AlgebraicGeometry.HasRingHomProperty.iff_appLE {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} : P f ↔ ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U), Q (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)

theorem AlgebraicGeometry.HasRingHomProperty.of_source_openCover {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.IsAffine Y] (𝒰 : X.OpenCover) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] (H : ∀ (i : 𝒰.J), Q (AlgebraicGeometry.Scheme.Hom.app (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) ⊤)) : P f

theorem AlgebraicGeometry.HasRingHomProperty.iff_of_source_openCover {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.IsAffine Y] (𝒰 : X.OpenCover) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] : P f ↔ ∀ (i : 𝒰.J), Q (AlgebraicGeometry.Scheme.Hom.app (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) ⊤)

theorem AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] : P f ↔ Q (AlgebraicGeometry.Scheme.Hom.app f ⊤)

theorem AlgebraicGeometry.HasRingHomProperty.Spec_iff {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] {R S : CommRingCat} {φ : R ⟶ S} : P (AlgebraicGeometry.Spec.map φ) ↔ Q φ

theorem AlgebraicGeometry.HasRingHomProperty.of_iSup_eq_top {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.IsAffine Y] {ι : Type u_1} (U : ι → ↑X.affineOpens) (hU : ⨆ (i : ι), ↑(U i) = ⊤) (H : ∀ (i : ι), Q (AlgebraicGeometry.Scheme.Hom.appLE f ⊤ ↑(U i) ⋯)) : P f

theorem AlgebraicGeometry.HasRingHomProperty.iff_of_iSup_eq_top {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.IsAffine Y] {ι : Type u_1} (U : ι → ↑X.affineOpens) (hU : ⨆ (i : ι), ↑(U i) = ⊤) : P f ↔ ∀ (i : ι), Q (AlgebraicGeometry.Scheme.Hom.appLE f ⊤ ↑(U i) ⋯)

instance AlgebraicGeometry.HasRingHomProperty.instIsLocalAtSource {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] : AlgebraicGeometry.IsLocalAtSource P

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.HasRingHomProperty.containsIdentities {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] (hP : RingHom.ContainsIdentities fun {R S : Type u} [CommRing R] [CommRing S] => Q) : P.ContainsIdentities

theorem AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty_of_isLocalAtSource_of_isLocalAtTarget (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocalAtTarget P] [AlgebraicGeometry.IsLocalAtSource P] : RingHom.PropertyIsLocal fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) => P (AlgebraicGeometry.Spec.map (CommRingCat.ofHom f))

theorem AlgebraicGeometry.HasRingHomProperty.of_isLocalAtSource_of_isLocalAtTarget (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocalAtTarget P] [AlgebraicGeometry.IsLocalAtSource P] : AlgebraicGeometry.HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) => P (AlgebraicGeometry.Spec.map (CommRingCat.ofHom f))

theorem AlgebraicGeometry.HasRingHomProperty.stalkwise {P : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.RespectsIso P) : AlgebraicGeometry.HasRingHomProperty (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] => P) fun {x S : Type u_1} {x_1 : CommRing x} {x_2 : CommRing S} (φ : x →+* S) => ∀ (p : Ideal S) (x_3 : p.IsPrime), P (Localization.localRingHom (Ideal.comap φ p) p φ ⋯)

theorem AlgebraicGeometry.HasRingHomProperty.stableUnderComposition {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] (hP : RingHom.StableUnderComposition fun {R S : Type u} [CommRing R] [CommRing S] => Q) : P.IsStableUnderComposition

theorem AlgebraicGeometry.HasRingHomProperty.of_comp {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] (H : ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T), Q (g.comp f) → Q g) {X Y Z : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {g : Y ⟶ Z} (h : P (CategoryTheory.CategoryStruct.comp f g)) : P f

theorem AlgebraicGeometry.HasRingHomProperty.isMultiplicative {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] (hPc : RingHom.StableUnderComposition fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hPi : RingHom.ContainsIdentities fun {R S : Type u} [CommRing R] [CommRing S] => Q) : P.IsMultiplicative

theorem AlgebraicGeometry.HasRingHomProperty.of_isOpenImmersion {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (hP : RingHom.ContainsIdentities fun {R S : Type u} [CommRing R] [CommRing S] => Q) [AlgebraicGeometry.IsOpenImmersion f] : P f

theorem AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChange {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] (hP : RingHom.IsStableUnderBaseChange fun {R S : Type u} [CommRing R] [CommRing S] => Q) : P.IsStableUnderBaseChange

theorem AlgebraicGeometry.HasRingHomProperty.respects_isOpenImmersion {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] (hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S : Type u} [CommRing R] [CommRing S] => Q) : P.Respects @AlgebraicGeometry.IsOpenImmersion

Any property of scheme morphisms induced by a property of ring homomorphisms is stable under composition with open immersions.

theorem AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE_locally {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQi : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) [AlgebraicGeometry.HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] => RingHom.Locally fun {R S : Type u} [CommRing R] [CommRing S] => Q] : P f ↔ ∀ (x : ↑↑X.toPresheafedSpace), ∃ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (_ : x ∈ ↑V) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U), Q (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)

If P is induced by Locally Q, it suffices to check Q on affine open sets locally around points of the source.

theorem AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S : Type u} [CommRing R] [CommRing S] => Q) : P f ↔ ∀ (x : ↑↑X.toPresheafedSpace), ∃ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (_ : x ∈ ↑V) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U), Q (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)

P can be checked locally around points of the source.

theorem AlgebraicGeometry.HasRingHomProperty.locally_of_iff {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQl : RingHom.LocalizationAwayPreserves fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQa : RingHom.StableUnderCompositionWithLocalizationAway fun {R S : Type u} [CommRing R] [CommRing S] => Q) (h : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), P f ↔ ∀ (x : ↑↑X.toPresheafedSpace), ∃ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (_ : x ∈ ↑V) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U), Q (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)) : AlgebraicGeometry.HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] => RingHom.Locally fun {R S : Type u} [CommRing R] [CommRing S] => Q