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

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

• One or more equations did not get rendered due to their size.

@[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.

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) : 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 ≤ f⁻¹ᵁ ↑U), P (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.toPrefunctor.obj (Opposite.op ⊤))) (H : AlgebraicGeometry.sourceAffineLocally P f) (U : ↑(AlgebraicGeometry.Scheme.affineOpens (X ∣_ᵤ f⁻¹ᵁ Y.basicOpen r))) : P (AlgebraicGeometry.Scheme.Γ.toPrefunctor.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ofRestrict (X ∣_ᵤ f⁻¹ᵁ Y.basicOpen r) (_ : OpenEmbedding ⇑(TopologicalSpace.Opens.inclusion ↑U))) (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.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.toPrefunctor.obj (Opposite.op ↑U))) (hs : Ideal.span s = ⊤) (hs' : ∀ (r : ↑s), P (AlgebraicGeometry.Scheme.Γ.toPrefunctor.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ιOpens (X.basicOpen ↑r)) f).op)) : P (AlgebraicGeometry.Scheme.Γ.toPrefunctor.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.Γ.toPrefunctor.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 (𝒰.obj i)] (H : ∀ (i : 𝒰.J), P (AlgebraicGeometry.Scheme.Γ.toPrefunctor.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) : List.TFAE [AlgebraicGeometry.sourceAffineLocally P f, ∃ (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (_ : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)), ∀ (i : 𝒰.J), P (AlgebraicGeometry.Scheme.Γ.toPrefunctor.map (CategoryTheory.CategoryStruct.comp (𝒰.map i) f).op), ∀ (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) [inst : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] (i : 𝒰.J), P (AlgebraicGeometry.Scheme.Γ.toPrefunctor.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.Γ.toPrefunctor.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, ∃ (𝒰 : AlgebraicGeometry.Scheme.OpenCover X), ∀ (i : 𝒰.J), AlgebraicGeometry.sourceAffineLocally P (CategoryTheory.CategoryStruct.comp (𝒰.map i) f), ∀ (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (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)]

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 (𝒰.obj i)] : AlgebraicGeometry.sourceAffineLocally P f ↔ ∀ (i : 𝒰.J), P (AlgebraicGeometry.Scheme.Γ.toPrefunctor.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.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 (𝒰.obj i)] (𝒰' : (i : (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f).J) → AlgebraicGeometry.Scheme.OpenCover ((AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f).obj i)) [∀ (i : (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f).J) (j : (𝒰' i).J), AlgebraicGeometry.IsAffine ((𝒰' i).obj j)] : AlgebraicGeometry.affineLocally P f ↔ ∀ (i : (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f).J) (j : (𝒰' i).J), P (AlgebraicGeometry.Scheme.Γ.toPrefunctor.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) (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) : 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 (RingHom.comp g 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_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)