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,

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 : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) (hP : RingHom.StableUnderBaseChange fun {R S : Type u} [CommRing R] [CommRing S] => P) (hP' : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => 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.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 ⋯)

Instances For

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

Instances For

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 : AlgebraicGeometry.Scheme} {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.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 : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) {X : AlgebraicGeometry.Scheme} {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.val.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.LocalizationPreserves 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

class AlgebraicGeometry.HasRingHomProperty (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (Q : outParam ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (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

Q is local (See RingHom.PropertyIsLocal)
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

Instances

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

RingHom.PropertyIsLocal fun {R S : Type u} [CommRing R] [CommRing S] => Q

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

P = AlgebraicGeometry.affineLocally 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)

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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (H : 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.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 : AlgebraicGeometry.Scheme} {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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {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 {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 : AlgebraicGeometry.Scheme} {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 : AlgebraicGeometry.Scheme} {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 : AlgebraicGeometry.Scheme} {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 : CommRingCat} {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 : AlgebraicGeometry.Scheme} {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 : AlgebraicGeometry.Scheme} {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.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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {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 : AlgebraicGeometry.Scheme} {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.stableUnderBaseChange {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.StableUnderBaseChange fun {R S : Type u} [CommRing R] [CommRing S] => Q) :

P.StableUnderBaseChange