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 : AlgebraicGeometry.Scheme} {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.app 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) :
    (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_stableUnderBaseChange {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.StableUnderBaseChange fun {R S : Type u} [CommRing R] [CommRing S] => Q) :
    (AlgebraicGeometry.affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q).StableUnderBaseChange

    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 : AlgebraicGeometry.Scheme} {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)
    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_stableUnderBaseChange {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) → (RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) → (RingHom.StableUnderBaseChange fun {R S : Type u} [CommRing R] [CommRing S] => Q) → P.StableUnderBaseChange

    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)

    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