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

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.diagonal_targetAffineLocally_of_openCover (P : AlgebraicGeometry.AffineTargetMorphismProperty) (hP : P.IsLocal) {X : AlgebraicGeometry.Scheme} {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), P (CategoryTheory.Limits.pullback.mapDesc ((𝒰' i).map j) ((𝒰' i).map k) CategoryTheory.Limits.pullback.snd)) : (AlgebraicGeometry.targetAffineLocally P).diagonal f

theorem AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_of_targetAffineLocally (P : AlgebraicGeometry.AffineTargetMorphismProperty) (hP : P.IsLocal) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {U : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : U ⟶ Y) [AlgebraicGeometry.IsAffine U] [AlgebraicGeometry.IsOpenImmersion g] (H : (AlgebraicGeometry.targetAffineLocally P).diagonal f) : P.diagonal CategoryTheory.Limits.pullback.snd

theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.diagonal_affine_openCover_TFAE {P : AlgebraicGeometry.AffineTargetMorphismProperty} (hP : P.IsLocal) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : [(AlgebraicGeometry.targetAffineLocally P).diagonal f, ∃ (𝒰 : Y.OpenCover) (x : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)), ∀ (i : 𝒰.J), P.diagonal CategoryTheory.Limits.pullback.snd, ∀ (𝒰 : Y.OpenCover) [inst : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] (i : 𝒰.J), P.diagonal CategoryTheory.Limits.pullback.snd, ∀ {U : AlgebraicGeometry.Scheme} (g : U ⟶ Y) [inst : AlgebraicGeometry.IsAffine U] [inst_1 : AlgebraicGeometry.IsOpenImmersion g], P.diagonal CategoryTheory.Limits.pullback.snd, ∃ (𝒰 : Y.OpenCover) (x : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)) (𝒰' : (i : 𝒰.J) → (CategoryTheory.Limits.pullback f (𝒰.map i)).OpenCover) (x_1 : ∀ (i : 𝒰.J) (j : (𝒰' i).J), AlgebraicGeometry.IsAffine ((𝒰' i).obj j)), ∀ (i : 𝒰.J) (j k : (𝒰' i).J), P (CategoryTheory.Limits.pullback.mapDesc ((𝒰' i).map j) ((𝒰' i).map k) CategoryTheory.Limits.pullback.snd)].TFAE

theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.diagonal {P : AlgebraicGeometry.AffineTargetMorphismProperty} (hP : P.IsLocal) : P.diagonal.IsLocal

theorem AlgebraicGeometry.diagonal_targetAffineLocally_eq_targetAffineLocally (P : AlgebraicGeometry.AffineTargetMorphismProperty) (hP : P.IsLocal) : (AlgebraicGeometry.targetAffineLocally P).diagonal = AlgebraicGeometry.targetAffineLocally P.diagonal

theorem AlgebraicGeometry.universally_isLocalAtTarget (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (hP : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover), (∀ (i : 𝒰.J), P CategoryTheory.Limits.pullback.snd) → P f) : AlgebraicGeometry.PropertyIsLocalAtTarget P.universally

theorem AlgebraicGeometry.universally_isLocalAtTarget_of_morphismRestrict (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [P.RespectsIso] (hP₂ : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f) : AlgebraicGeometry.PropertyIsLocalAtTarget P.universally

def AlgebraicGeometry.MorphismProperty.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.MorphismProperty.topologically P f = P ⇑f.val.base

theorem AlgebraicGeometry.MorphismProperty.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.MorphismProperty.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.MorphismProperty.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.MorphismProperty.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.MorphismProperty.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.MorphismProperty.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.MorphismProperty.topologically_propertyIsLocalAtTarget (P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop) [(AlgebraicGeometry.MorphismProperty.topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso] (hP₂ : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β), 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.PropertyIsLocalAtTarget (AlgebraicGeometry.MorphismProperty.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.

def AlgebraicGeometry.MorphismProperty.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.MorphismProperty.stalkwise P f = ∀ (x_1 : ↑↑x✝.toPresheafedSpace), P (AlgebraicGeometry.PresheafedSpace.stalkMap f.val x_1)

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

If P respects isos, then stalkwise P respects isos.

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

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

def AlgebraicGeometry.AffineTargetMorphismProperty.of (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) : AlgebraicGeometry.AffineTargetMorphismProperty

If P is a property of scheme morphisms, we may restrict P to morphisms with affine target to obtain an AffineTargetMorphismProperty.

Equations

• AlgebraicGeometry.AffineTargetMorphismProperty.of P f = P f

theorem AlgebraicGeometry.AffineTargetMorphismProperty.targetAffineLocally_of_eq_of_isLocalAtTarget (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (hP : AlgebraicGeometry.PropertyIsLocalAtTarget P) : AlgebraicGeometry.targetAffineLocally (AlgebraicGeometry.AffineTargetMorphismProperty.of P) = P

Restricting a local at the target morphism property of schemes P to morphisms with affine target and extending to a global property with targetAffineLocally yields P again, if P is local at the target.

theorem AlgebraicGeometry.AffineTargetMorphismProperty.of_isLocal_of_isLocalAtTarget (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (hP : AlgebraicGeometry.PropertyIsLocalAtTarget P) : (AlgebraicGeometry.AffineTargetMorphismProperty.of P).IsLocal

The restriction of a morphism property of schemes that is local at the target to morphisms with affine target, is local.

theorem AlgebraicGeometry.AffineTargetMorphismProperty.stableUnderBaseChange_of_stableUnderBaseChangeOnAffine_of_isLocalAtTarget (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (hP₁ : AlgebraicGeometry.PropertyIsLocalAtTarget P) (hP₂ : (AlgebraicGeometry.AffineTargetMorphismProperty.of P).StableUnderBaseChange) : P.StableUnderBaseChange

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.diagonal_targetAffineLocally_of_openCover]

theorem AlgebraicGeometry.diagonalTargetAffineLocallyOfOpenCover (P : AlgebraicGeometry.AffineTargetMorphismProperty) (hP : P.IsLocal) {X : AlgebraicGeometry.Scheme} {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), P (CategoryTheory.Limits.pullback.mapDesc ((𝒰' i).map j) ((𝒰' i).map k) CategoryTheory.Limits.pullback.snd)) : (AlgebraicGeometry.targetAffineLocally P).diagonal f

Alias of AlgebraicGeometry.diagonal_targetAffineLocally_of_openCover.

@[deprecated AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_of_targetAffineLocally]

theorem AlgebraicGeometry.AffineTargetMorphismProperty.diagonalOfTargetAffineLocally (P : AlgebraicGeometry.AffineTargetMorphismProperty) (hP : P.IsLocal) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {U : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : U ⟶ Y) [AlgebraicGeometry.IsAffine U] [AlgebraicGeometry.IsOpenImmersion g] (H : (AlgebraicGeometry.targetAffineLocally P).diagonal f) : P.diagonal CategoryTheory.Limits.pullback.snd

Alias of AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_of_targetAffineLocally.

@[deprecated AlgebraicGeometry.universally_isLocalAtTarget]

theorem AlgebraicGeometry.universallyIsLocalAtTarget (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (hP : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover), (∀ (i : 𝒰.J), P CategoryTheory.Limits.pullback.snd) → P f) : AlgebraicGeometry.PropertyIsLocalAtTarget P.universally

Alias of AlgebraicGeometry.universally_isLocalAtTarget.

@[deprecated AlgebraicGeometry.universally_isLocalAtTarget_of_morphismRestrict]

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

Alias of AlgebraicGeometry.universally_isLocalAtTarget_of_morphismRestrict.