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

We also provide the instances P.IsMultiplicative, P.IsStableUnderComposition, IsLocalAtTarget P, IsLocalAtSource P.

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
Instances For
    @[reducible, inline]
    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.

    Equations
    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

      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.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) :
        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_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) )
        Equations
        • =
        Equations
        • =
        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
        Equations
        • =