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

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

• AlgebraicGeometry.affineAnd Q f = (AlgebraicGeometry.IsAffine X ∧ Q (AlgebraicGeometry.Scheme.Hom.app f ⊤))

@[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.app f ⊤)

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.

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.

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.

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)

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)

Variant of targetAffineLocally_affineAnd_iff where IsAffineHom is bundled.

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

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

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)

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.

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.

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.

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.

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

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'

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'