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) :
AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffine Y] :
    AlgebraicGeometry.affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] => Q) f ↔ AlgebraicGeometry.IsAffine X ∧ Q (AlgebraicGeometry.Scheme.Hom.appTop f).hom
    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) :
    (AlgebraicGeometry.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.LocalizationPreserves fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQs : RingHom.OfLocalizationSpan fun {R S : Type u} [CommRing R] [CommRing S] => Q) :
    (AlgebraicGeometry.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_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) :
    (AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
    AlgebraicGeometry.targetAffineLocally (AlgebraicGeometry.affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q) f ↔ ∀ (U : Y.Opens), AlgebraicGeometry.IsAffineOpen U → AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U) ∧ Q (AlgebraicGeometry.Scheme.Hom.app f U).hom
    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 : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
    AlgebraicGeometry.targetAffineLocally (AlgebraicGeometry.affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q) f ↔ AlgebraicGeometry.IsAffineHom f ∧ ∀ (U : Y.Opens), AlgebraicGeometry.IsAffineOpen U → Q (AlgebraicGeometry.Scheme.Hom.app f U).hom

    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 : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
    AlgebraicGeometry.targetAffineLocally (AlgebraicGeometry.affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q) f ↔ AlgebraicGeometry.IsAffineHom f ∧ AlgebraicGeometry.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) :
    AlgebraicGeometry.targetAffineLocally (AlgebraicGeometry.affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q) = @AlgebraicGeometry.IsAffineHom ⊓ AlgebraicGeometry.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) :
    AlgebraicGeometry.targetAffineLocally (AlgebraicGeometry.affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q) ≤ AlgebraicGeometry.targetAffineLocally (AlgebraicGeometry.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 AlgebraicGeometry.Scheme} (hA : AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.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 AlgebraicGeometry.Scheme} :
    AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.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 AlgebraicGeometry.Scheme} (hA : AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.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 AlgebraicGeometry.Scheme) (hQi : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQl : RingHom.LocalizationPreserves fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQs : RingHom.OfLocalizationSpan fun {R S : Type u} [CommRing R] [CommRing S] => Q) :
    AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q) ↔ ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), P f ↔ AlgebraicGeometry.IsAffineHom f ∧ ∀ (U : Y.Opens), AlgebraicGeometry.IsAffineOpen U → Q (AlgebraicGeometry.Scheme.Hom.app f U).hom

    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 AlgebraicGeometry.Scheme) (hA : AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q)) :
    P ≤ @AlgebraicGeometry.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 AlgebraicGeometry.Scheme} (hP : AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q)) [AlgebraicGeometry.HasRingHomProperty P' fun {R S : Type u} [CommRing R] [CommRing S] => Q] :
    P = @AlgebraicGeometry.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 AlgebraicGeometry.Scheme} (hP : AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q)) (hP' : AlgebraicGeometry.HasAffineProperty P' (AlgebraicGeometry.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'