Constructors for properties of morphisms between schemes

This file provides some constructors to obtain morphism properties of schemes from other morphism properties:

• AffineTargetMorphismProperty.diagonal : Given an affine target morphism property P, P.diagonal f holds if P (pullback.mapDesc f₁ f₂ f) holds for two affine open immersions f₁ and f₂.
• AffineTargetMorphismProperty.of: Given a morphism property P of schemes, this is the restriction of P to morphisms with affine target. If P is local at the target, we have (toAffineTargetMorphismProperty P).targetAffineLocally = P (see MorphismProperty.targetAffineLocally_toAffineTargetMorphismProperty_eq_of_isLocalAtTarget).
• MorphismProperty.topologically: Given a property P of maps of topological spaces, (topologically P) f holds if P holds for the underlying continuous map of f.
• MorphismProperty.stalkwise: Given a property P of ring homs, (stalkwise P) f holds if P holds for all stalk maps.

Also provides API for showing the standard locality and stability properties for these types of properties.

def AlgebraicGeometry.AffineTargetMorphismProperty.diagonal (P : AffineTargetMorphismProperty) : AffineTargetMorphismProperty

The AffineTargetMorphismProperty associated to (targetAffineLocally P).diagonal. See diagonal_targetAffineLocally_eq_targetAffineLocally.

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_respectsIso (P : AffineTargetMorphismProperty) [P.toProperty.RespectsIso] : P.diagonal.toProperty.RespectsIso

theorem AlgebraicGeometry.HasAffineProperty.diagonal_of_openCover (P : CategoryTheory.MorphismProperty Scheme) {Q : AffineTargetMorphismProperty} [HasAffineProperty P Q] {X Y : Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) [∀ (i : 𝒰.J), IsAffine (𝒰.obj i)] (𝒰' : (i : 𝒰.J) → (CategoryTheory.Limits.pullback f (𝒰.map i)).OpenCover) [∀ (i : 𝒰.J) (j : (𝒰' i).J), IsAffine ((𝒰' i).obj j)] (h𝒰' : ∀ (i : 𝒰.J) (j k : (𝒰' i).J), Q (CategoryTheory.Limits.pullback.mapDesc ((𝒰' i).map j) ((𝒰' i).map k) (Scheme.Cover.pullbackHom 𝒰 f i))) : P.diagonal f

theorem AlgebraicGeometry.HasAffineProperty.diagonal_of_openCover_diagonal (P : CategoryTheory.MorphismProperty Scheme) {Q : AffineTargetMorphismProperty} [HasAffineProperty P Q] {X Y : Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) [∀ (i : 𝒰.J), IsAffine (𝒰.obj i)] (h𝒰 : ∀ (i : 𝒰.1), Q.diagonal (Scheme.Cover.pullbackHom 𝒰 f i)) : P.diagonal f

theorem AlgebraicGeometry.HasAffineProperty.diagonal_of_diagonal_of_isPullback (P : CategoryTheory.MorphismProperty Scheme) {Q : AffineTargetMorphismProperty} [HasAffineProperty P Q] {X Y U V : Scheme} {f : X ⟶ Y} {g : U ⟶ Y} [IsAffine U] [IsOpenImmersion g] {iV : V ⟶ X} {f' : V ⟶ U} (h : CategoryTheory.IsPullback iV f' f g) (H : P.diagonal f) : Q.diagonal f'

theorem AlgebraicGeometry.HasAffineProperty.diagonal_iff (P : CategoryTheory.MorphismProperty Scheme) {Q : AffineTargetMorphismProperty} [HasAffineProperty P Q] {X Y : Scheme} {f : X ⟶ Y} [IsAffine Y] : Q.diagonal f ↔ P.diagonal f

instance AlgebraicGeometry.HasAffineProperty.diagonal_affineProperty_isLocal {Q : AffineTargetMorphismProperty} [Q.IsLocal] : Q.diagonal.IsLocal

instance AlgebraicGeometry.instHasAffinePropertyDiagonalSchemeDiagonal (P : CategoryTheory.MorphismProperty Scheme) {Q : AffineTargetMorphismProperty} [HasAffineProperty P Q] : HasAffineProperty P.diagonal Q.diagonal

instance AlgebraicGeometry.instIsLocalAtTargetDiagonalScheme (P : CategoryTheory.MorphismProperty Scheme) [IsLocalAtTarget P] : IsLocalAtTarget P.diagonal

instance AlgebraicGeometry.instIsLocalAtSourceDiagonalSchemeOfHasOfPostcompPropertyOfRespectsRightIsOpenImmersion (P : CategoryTheory.MorphismProperty Scheme) [P.HasOfPostcompProperty @IsOpenImmersion] [P.RespectsRight @IsOpenImmersion] [IsLocalAtSource P] : IsLocalAtSource P.diagonal

theorem AlgebraicGeometry.universally_isLocalAtTarget (P : CategoryTheory.MorphismProperty Scheme) (hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f) : IsLocalAtTarget P.universally

def AlgebraicGeometry.topologically (P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop) : CategoryTheory.MorphismProperty Scheme

topologically P holds for a morphism if the underlying topological map satisfies P.

Equations

• AlgebraicGeometry.topologically P f = P ⇑(CategoryTheory.ConcreteCategory.hom f.base)

theorem AlgebraicGeometry.topologically_isStableUnderComposition (P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop) (hP : ∀ {α β γ : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (f : α → β) (g : β → γ), P f → P g → P (g ∘ f)) : (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => P).IsStableUnderComposition

If a property of maps of topological spaces is stable under composition, the induced morphism property of schemes is stable under composition.

theorem AlgebraicGeometry.topologically_iso_le (P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop) (hP : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β), P ⇑f) : CategoryTheory.MorphismProperty.isomorphisms Scheme ≤ topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => P

If a property of maps of topological spaces is satisfied by all homeomorphisms, every isomorphism of schemes satisfies the induced property.

theorem AlgebraicGeometry.topologically_respectsIso (P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop) (hP₁ : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β), P ⇑f) (hP₂ : ∀ {α β γ : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (f : α → β) (g : β → γ), P f → P g → P (g ∘ f)) : (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso

If a property of maps of topological spaces is satisfied by homeomorphisms and is stable under composition, the induced property on schemes respects isomorphisms.

theorem AlgebraicGeometry.topologically_isLocalAtTarget (P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop) [(topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso] (hP₂ : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β), Continuous f → IsOpen s → P f → P (s.restrictPreimage f)) (hP₃ : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → TopologicalSpace.Opens β), iSup U = ⊤ → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f) : IsLocalAtTarget (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => P)

To check that a topologically defined morphism property is local at the target, we may check the corresponding properties on topological spaces.

theorem AlgebraicGeometry.topologically_isLocalAtTarget' (P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop) [(topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso] (hP : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → TopologicalSpace.Opens β), iSup U = ⊤ → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))) : IsLocalAtTarget (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => P)

A variant of topologically_isLocalAtTarget that takes one iff statement instead of two implications.

def AlgebraicGeometry.stalkwise (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : CategoryTheory.MorphismProperty Scheme

stalkwise P holds for a morphism if all stalks satisfy P.

Equations

• AlgebraicGeometry.stalkwise P f = ∀ (x : ↑↑x✝¹.toPresheafedSpace), P (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x))

theorem AlgebraicGeometry.stalkwise_respectsIso {P : {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] => P) : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] => P).RespectsIso

If P respects isos, then stalkwise P respects isos.

theorem AlgebraicGeometry.stalkwiseIsLocalAtTarget_of_respectsIso {P : {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] => P) : IsLocalAtTarget (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] => P)

If P respects isos, then stalkwise P is local at the target.

theorem AlgebraicGeometry.stalkwise_isLocalAtSource_of_respectsIso {P : {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] => P) : IsLocalAtSource (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] => P)

If P respects isos, then stalkwise P is local at the source.

theorem AlgebraicGeometry.stalkwise_Spec_map_iff {P : {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] => P) {R S : CommRingCat} (φ : R ⟶ S) : stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] => P) (Spec.map φ) ↔ ∀ (p : Ideal ↑S) (x : p.IsPrime), P (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p) p (CommRingCat.Hom.hom φ) ⋯)

theorem AlgebraicGeometry.AffineTargetMorphismProperty.isStableUnderBaseChange_of_isStableUnderBaseChangeOnAffine_of_isLocalAtTarget (P : CategoryTheory.MorphismProperty Scheme) [IsLocalAtTarget P] (hP₂ : (of P).IsStableUnderBaseChange) : P.IsStableUnderBaseChange

If P is local at the target, to show that P is stable under base change, it suffices to check this for base change along a morphism of affine schemes.