Documentation

Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

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,

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 ))) :
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)

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.

Instances For
    @[inline, reducible]
    abbrev AlgebraicGeometry.affineLocally (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (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.

    Instances For
      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_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)) :
      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.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)] :
      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)) :