Documentation

Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Affine morphisms with additional ring hom property #

In this file we define a constructor affineAnd Q for affine target morphism properties of schemes from a property of ring homomorphisms Q: A morphism f : X ⟶ Y with affine target satisfies affineAnd Q if it is an affine morphim (i.e. X is affine) and the induced ring map on global sections satisfies Q.

affineAnd Q inherits most stability properties of Q and is local at the target if Q is local at the (algebraic) source.

Typical examples of this are affine morphisms (where Q is trivial), finite morphisms (where Q is module finite) or closed immersions (where Q is being surjective).

source
def AlgebraicGeometry.affineAnd (Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) :
AffineTargetMorphismProperty

This is the affine target morphism property where the source is affine and the induced map of rings on global sections satisfies P.

Equations
Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.affineAnd_apply (Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) {X Y : Scheme} (f : X ⟶ Y) [IsAffine Y] :
    affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] => Q) f ↔ IsAffine X ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
    source
    theorem AlgebraicGeometry.affineAnd_respectsIso {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) :
    (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q).toProperty.RespectsIso

    If P respects isos, also affineAnd P respects isomorphisms.

    source
    theorem AlgebraicGeometry.affineAnd_isLocal {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hPi : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQl : RingHom.LocalizationAwayPreserves fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQs : RingHom.OfLocalizationSpan fun {R S : Type u} [CommRing R] [CommRing S] => Q) :
    (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q).IsLocal

    affineAnd P is local if P is local on the (algebraic) source.

    source
    theorem AlgebraicGeometry.affineAnd_isLocal_of_propertyIsLocal {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hPi : RingHom.PropertyIsLocal fun {R S : Type u} [CommRing R] [CommRing S] => Q) :
    (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q).IsLocal
    source
    theorem AlgebraicGeometry.affineAnd_isStableUnderBaseChange {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQb : RingHom.IsStableUnderBaseChange fun {R S : Type u} [CommRing R] [CommRing S] => Q) :
    (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q).IsStableUnderBaseChange

    If P is stable under base change, so is affineAnd P.

    source
    theorem AlgebraicGeometry.targetAffineLocally_affineAnd_iff {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) {X Y : Scheme} (f : X ⟶ Y) :
    targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q) f ↔ ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
    source
    theorem AlgebraicGeometry.targetAffineLocally_affineAnd_iff' {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) {X Y : Scheme} (f : X ⟶ Y) :
    targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q) f ↔ IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

    Variant of targetAffineLocally_affineAnd_iff where IsAffineHom is bundled.

    source
    theorem AlgebraicGeometry.targetAffineLocally_affineAnd_iff_affineLocally {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQ : RingHom.PropertyIsLocal fun {R S : Type u} [CommRing R] [CommRing S] => Q) {X Y : Scheme} (f : X ⟶ Y) :
    targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q) f ↔ IsAffineHom f ∧ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] => Q) f
    source
    theorem AlgebraicGeometry.targetAffineLocally_affineAnd_eq_affineLocally {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQ : RingHom.PropertyIsLocal fun {R S : Type u} [CommRing R] [CommRing S] => Q) :
    targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q) = @IsAffineHom ⊓ affineLocally fun {R S : Type u} [CommRing R] [CommRing S] => Q
    source
    theorem AlgebraicGeometry.targetAffineLocally_affineAnd_le {Q W : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQW : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → W f) :
    targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q) ≤ targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => W)
    source
    theorem AlgebraicGeometry.HasAffineProperty.affineAnd_isStableUnderComposition {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : CategoryTheory.MorphismProperty Scheme} (hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q)) (hQ : RingHom.StableUnderComposition fun {R S : Type u} [CommRing R] [CommRing S] => Q) :
    P.IsStableUnderComposition

    If P is a morphism property affine locally defined by affineAnd Q, P is stable under composition if Q is.

    source
    theorem AlgebraicGeometry.HasAffineProperty.affineAnd_isStableUnderBaseChange {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : CategoryTheory.MorphismProperty Scheme} :
    HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q) → ∀ (hQi : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQb : RingHom.IsStableUnderBaseChange fun {R S : Type u} [CommRing R] [CommRing S] => Q), P.IsStableUnderBaseChange

    If P is a morphism property affine locally defined by affineAnd Q, P is stable under base change if Q is.

    source
    theorem AlgebraicGeometry.HasAffineProperty.affineAnd_containsIdentities {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : CategoryTheory.MorphismProperty Scheme} (hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q)) (hQi : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQ : RingHom.ContainsIdentities fun {R S : Type u} [CommRing R] [CommRing S] => Q) :
    P.ContainsIdentities

    If Q contains identities and respects isomorphisms (i.e. is satisfied by isomorphisms), and P is affine locally defined by affineAnd Q, then P contains identities.

    source
    theorem AlgebraicGeometry.HasAffineProperty.affineAnd_iff {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (P : CategoryTheory.MorphismProperty Scheme) (hQi : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQl : RingHom.LocalizationAwayPreserves fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQs : RingHom.OfLocalizationSpan fun {R S : Type u} [CommRing R] [CommRing S] => Q) :
    HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q) ↔ ∀ {X Y : Scheme} (f : X ⟶ Y), P f ↔ IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

    A convenience constructor for HasAffineProperty P (affineAnd Q). The IsAffineHom is bundled, since this goes well with defining morphism properties via extends IsAffineHom.

    source
    theorem AlgebraicGeometry.HasAffineProperty.affineAnd_le_isAffineHom {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (P : CategoryTheory.MorphismProperty Scheme) (hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q)) :
    P ≤ @IsAffineHom
    source
    theorem AlgebraicGeometry.HasAffineProperty.affineAnd_eq_of_propertyIsLocal {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P P' : CategoryTheory.MorphismProperty Scheme} (hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q)) [HasRingHomProperty P' fun {R S : Type u} [CommRing R] [CommRing S] => Q] :
    P = @IsAffineHom ⊓ P'
    source
    theorem AlgebraicGeometry.HasAffineProperty.affineAnd_le_affineAnd {Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P P' : CategoryTheory.MorphismProperty Scheme} (hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q)) (hP' : HasAffineProperty P' (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q')) (hQQ' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → Q' f) :
    P ≤ P'