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 : AlgebraicGeometry.AffineTargetMorphismProperty) : AlgebraicGeometry.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 : AlgebraicGeometry.AffineTargetMorphismProperty) [P.toProperty.RespectsIso] : P.diagonal.toProperty.RespectsIso

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

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

theorem AlgebraicGeometry.HasAffineProperty.diagonal_of_diagonal_of_isPullback (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {Q : AlgebraicGeometry.AffineTargetMorphismProperty} [AlgebraicGeometry.HasAffineProperty P Q] {X Y U V : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {g : U ⟶ Y} [AlgebraicGeometry.IsAffine U] [AlgebraicGeometry.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 AlgebraicGeometry.Scheme) {Q : AlgebraicGeometry.AffineTargetMorphismProperty} [AlgebraicGeometry.HasAffineProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.IsAffine Y] : Q.diagonal f ↔ P.diagonal f

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

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

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

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

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

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

Equations

• AlgebraicGeometry.topologically P f = P ⇑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)) : (AlgebraicGeometry.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 AlgebraicGeometry.Scheme ≤ AlgebraicGeometry.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)) : (AlgebraicGeometry.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) [(AlgebraicGeometry.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) : AlgebraicGeometry.IsLocalAtTarget (AlgebraicGeometry.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) [(AlgebraicGeometry.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))) : AlgebraicGeometry.IsLocalAtTarget (AlgebraicGeometry.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 AlgebraicGeometry.Scheme

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

Equations

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

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

theorem AlgebraicGeometry.AffineTargetMorphismProperty.isStableUnderBaseChange_of_isStableUnderBaseChangeOnAffine_of_isLocalAtTarget (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocalAtTarget P] (hP₂ : (AlgebraicGeometry.AffineTargetMorphismProperty.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.

@[deprecated AlgebraicGeometry.HasAffineProperty.diagonal_of_openCover]

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

Alias of AlgebraicGeometry.HasAffineProperty.diagonal_of_openCover.

@[deprecated AlgebraicGeometry.HasAffineProperty.diagonal_of_diagonal_of_isPullback]

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

Alias of AlgebraicGeometry.HasAffineProperty.diagonal_of_diagonal_of_isPullback.

@[deprecated AlgebraicGeometry.universally_isLocalAtTarget]

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

Alias of AlgebraicGeometry.universally_isLocalAtTarget.

@[deprecated AlgebraicGeometry.universally_isLocalAtTarget]

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

Alias of AlgebraicGeometry.universally_isLocalAtTarget.