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 { unop := ⊤ })) : P (AlgebraicGeometry.Scheme.Γ.map (f ∣_ Y.basicOpen r).op) ↔ P (IsLocalization.Away.map (↑(Y.presheaf.obj { unop := Y.basicOpen r })) (↑(X.presheaf.obj { unop := X.basicOpen ((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 { unop := ⊤ })) : P (AlgebraicGeometry.Scheme.Γ.map (f ∣_ Y.basicOpen r).op) ↔ P (Localization.awayMap (AlgebraicGeometry.Scheme.Γ.map f.op) r)

@[deprecated RingHom.RespectsIso.basicOpen_iff_localization]

theorem RingHom.RespectsIso.ofRestrict_morphismRestrict_iff_of_isAffine {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 { unop := ⊤ })) : P (AlgebraicGeometry.Scheme.Γ.map (f ∣_ Y.basicOpen r).op) ↔ P (Localization.awayMap (AlgebraicGeometry.Scheme.Γ.map f.op) r)

Alias of RingHom.RespectsIso.basicOpen_iff_localization.

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 { unop := ⊤ })) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hU : AlgebraicGeometry.IsAffineOpen U) {V : TopologicalSpace.Opens ↑↑(X ∣_ᵤ (TopologicalSpace.Opens.map f.val.base).obj (Y.basicOpen r)).toPresheafedSpace} (e : V = (TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.ιOpens ((TopologicalSpace.Opens.map f.val.base).obj (Y.basicOpen r))).val.base).obj U) : P (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ιOpens V) (f ∣_ Y.basicOpen r)).op) ↔ P (Localization.awayMap (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ιOpens 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.Γ.map g.op)) : P (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.

Equations

• AlgebraicGeometry.sourceAffineLocally P f = ∀ (U : ↑X.affineOpens), P (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp (X.ofRestrict ⋯) f).op)

@[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 P)

theorem AlgebraicGeometry.sourceAffineLocally_respectsIso {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (h₁ : RingHom.RespectsIso P) : (AlgebraicGeometry.sourceAffineLocally 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 P) : (AlgebraicGeometry.affineLocally P).RespectsIso

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 : ↑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.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 { unop := ⊤ })) (H : AlgebraicGeometry.sourceAffineLocally P f) (U : ↑(X ∣_ᵤ (TopologicalSpace.Opens.map f.val.base).obj (Y.basicOpen r)).affineOpens) : P (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp ((X ∣_ᵤ (TopologicalSpace.Opens.map f.val.base).obj (Y.basicOpen r)).ofRestrict ⋯) (f ∣_ Y.basicOpen 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.sourceAffineLocally P).IsLocal

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 : ↑X.affineOpens) (s : Set ↑(X.presheaf.obj { unop := ↑U })) (hs : Ideal.span s = ⊤) (hs' : ∀ (r : ↑s), P (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ιOpens (X.basicOpen ↑r)) f).op)) : P (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ιOpens ↑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.Γ.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] (𝒰 : X.OpenCover) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] (H : ∀ (i : 𝒰.J), P (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp (𝒰.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) : [AlgebraicGeometry.sourceAffineLocally P f, ∃ (𝒰 : X.OpenCover) (_ : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)), ∀ (i : 𝒰.J), P (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp (𝒰.map i) f).op), ∀ (𝒰 : X.OpenCover) [inst : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] (i : 𝒰.J), P (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp (𝒰.map i) f).op), ∀ {U : AlgebraicGeometry.Scheme} (g : U ⟶ X) [inst : AlgebraicGeometry.IsAffine U] [inst : AlgebraicGeometry.IsOpenImmersion g], P (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp g f).op)].TFAE

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) : [AlgebraicGeometry.sourceAffineLocally P f, ∃ (𝒰 : X.OpenCover), ∀ (i : 𝒰.J), AlgebraicGeometry.sourceAffineLocally P (CategoryTheory.CategoryStruct.comp (𝒰.map i) f), ∀ (𝒰 : X.OpenCover) (i : 𝒰.J), AlgebraicGeometry.sourceAffineLocally P (CategoryTheory.CategoryStruct.comp (𝒰.map i) f), ∀ {U : AlgebraicGeometry.Scheme} (g : U ⟶ X) [inst : AlgebraicGeometry.IsOpenImmersion g], AlgebraicGeometry.sourceAffineLocally P (CategoryTheory.CategoryStruct.comp g f)].TFAE

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] (𝒰 : X.OpenCover) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] : AlgebraicGeometry.sourceAffineLocally P f ↔ ∀ (i : 𝒰.J), P (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp (𝒰.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.sourceAffineLocally P).IsLocal

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) (𝒰 : Y.OpenCover) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] (𝒰' : (i : (𝒰.pullbackCover f).J) → ((𝒰.pullbackCover f).obj i).OpenCover) [∀ (i : (𝒰.pullbackCover f).J) (j : (𝒰' i).J), AlgebraicGeometry.IsAffine ((𝒰' i).obj j)] : AlgebraicGeometry.affineLocally P f ↔ ∀ (i : (𝒰.pullbackCover f).J) (j : (𝒰' i).J), P (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp ((𝒰' i).map 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) (𝒰 : X.OpenCover) : AlgebraicGeometry.affineLocally P f ↔ ∀ (i : 𝒰.J), AlgebraicGeometry.affineLocally P (CategoryTheory.CategoryStruct.comp (𝒰.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 (g.comp f) → P 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_isStableUnderComposition {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.PropertyIsLocal P) : (AlgebraicGeometry.affineLocally P).IsStableUnderComposition