# 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. 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.stableUnderBaseChange: 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.StableUnderBaseChange.pullback_fst_app_top (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop) (hP : RingHom.StableUnderBaseChange fun {R S : Type u} [] [] => P) (hP' : RingHom.RespectsIso fun {R S : Type u} [] [] => P) (f : X S) (g : Y S) (H : ) :
def AlgebraicGeometry.sourceAffineLocally (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop) :

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
• = ∀ (U : X.affineOpens), P
Instances For
@[reducible, inline]
abbrev AlgebraicGeometry.affineLocally (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop) :

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
Instances For
theorem AlgebraicGeometry.sourceAffineLocally_respectsIso (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop) (h₁ : RingHom.RespectsIso fun {R S : Type u} [] [] => P) :
(AlgebraicGeometry.sourceAffineLocally fun {R S : Type u} [] [] => P).toProperty.RespectsIso
theorem AlgebraicGeometry.affineLocally_respectsIso (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop) (h : RingHom.RespectsIso fun {R S : Type u} [] [] => P) :
(AlgebraicGeometry.affineLocally fun {R S : Type u} [] [] => P).RespectsIso
theorem AlgebraicGeometry.sourceAffineLocally_morphismRestrict (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop) (f : X Y) (U : Y.Opens) (hU : ) :
AlgebraicGeometry.sourceAffineLocally (fun {R S : Type u} [] [] => P) (f ∣_ U) ∀ (V : X.affineOpens) (e : V (TopologicalSpace.Opens.map f.val.base).obj U), P (AlgebraicGeometry.Scheme.Hom.appLE f U (↑V) e)
theorem AlgebraicGeometry.affineLocally_iff_affineOpens_le (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop) (f : X Y) :
AlgebraicGeometry.affineLocally (fun {R S : Type u} [] [] => P) f ∀ (U : Y.affineOpens) (V : X.affineOpens) (e : V (TopologicalSpace.Opens.map f.val.base).obj U), P (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)
theorem AlgebraicGeometry.sourceAffineLocally_isLocal (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop) (h₁ : RingHom.RespectsIso fun {R S : Type u} [] [] => P) (h₂ : RingHom.LocalizationPreserves fun {R S : Type u} [] [] => P) (h₃ : RingHom.OfLocalizationSpan fun {R S : Type u} [] [] => P) :
(AlgebraicGeometry.sourceAffineLocally fun {R S : Type u} [] [] => P).IsLocal
class AlgebraicGeometry.HasRingHomProperty (Q : outParam ({R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)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.
Instances
theorem AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty {Q : outParam ({R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop)} [self : ] :
RingHom.PropertyIsLocal fun {R S : Type u} [] [] => Q
theorem AlgebraicGeometry.HasRingHomProperty.eq_affineLocally' {Q : outParam ({R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop)} [self : ] :
P = AlgebraicGeometry.affineLocally fun {R S : Type u} [] [] => Q
theorem AlgebraicGeometry.HasRingHomProperty.eq_affineLocally {Q : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} :
P = AlgebraicGeometry.affineLocally fun {R S : Type u} [] [] => Q
theorem AlgebraicGeometry.HasRingHomProperty.HasAffineProperty {Q : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} :
theorem AlgebraicGeometry.HasRingHomProperty.appLE {Q : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} (f : X Y) (H : P f) (U : Y.affineOpens) (V : X.affineOpens) (e : V (TopologicalSpace.Opens.map f.val.base).obj U) :
theorem AlgebraicGeometry.HasRingHomProperty.app_top {Q : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} (f : X Y) (H : P f) :
theorem AlgebraicGeometry.HasRingHomProperty.comp_of_isOpenImmersion {Q : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} (f : X Y) (g : Y Z) (H : P g) :
theorem AlgebraicGeometry.HasRingHomProperty.iff_appLE {Q : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} {f : X Y} :
P f ∀ (U : Y.affineOpens) (V : X.affineOpens) (e : V (TopologicalSpace.Opens.map f.val.base).obj U), Q (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)
theorem AlgebraicGeometry.HasRingHomProperty.of_source_openCover {Q : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} {f : X Y} (𝒰 : X.OpenCover) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] (H : ∀ (i : 𝒰.J), Q ) :
P f
theorem AlgebraicGeometry.HasRingHomProperty.iff_of_source_openCover {Q : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} {f : X Y} (𝒰 : X.OpenCover) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] :
P f ∀ (i : 𝒰.J), Q
theorem AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine {Q : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} {f : X Y} :
P f
theorem AlgebraicGeometry.HasRingHomProperty.Spec_iff {Q : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} {R : CommRingCat} {S : CommRingCat} {φ : R S} :
Q φ
theorem AlgebraicGeometry.HasRingHomProperty.of_iSup_eq_top {Q : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} {f : X 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 {Q : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} {f : X 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 {Q : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} :
Equations
• =
instance AlgebraicGeometry.HasRingHomProperty.instContainsIdentitiesScheme {Q : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} :
P.ContainsIdentities
Equations
• =
instance AlgebraicGeometry.HasRingHomProperty.instIsStableUnderCompositionScheme {Q : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} :
P.IsStableUnderComposition
Equations
• =
theorem AlgebraicGeometry.HasRingHomProperty.of_comp {Q : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} (H : ∀ {R S T : Type u} [inst : ] [inst_1 : ] [inst_2 : ] (f : R →+* S) (g : S →+* T), Q (g.comp f)Q g) {f : X Y} {g : Y Z} (h : ) :
P f
instance AlgebraicGeometry.HasRingHomProperty.instIsMultiplicativeScheme {Q : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} :
P.IsMultiplicative
Equations
• =
theorem AlgebraicGeometry.HasRingHomProperty.of_isOpenImmersion {Q : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} {f : X Y} :
P f
theorem AlgebraicGeometry.HasRingHomProperty.stableUnderBaseChange {Q : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} (hP : RingHom.StableUnderBaseChange fun {R S : Type u} [] [] => Q) :
P.StableUnderBaseChange