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_isZariskiLocalAtTarget
• 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 homomorphisms, (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.

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 : 𝒰.I₀), IsAffine (𝒰.X i)] (𝒰' : (i : 𝒰.I₀) → (CategoryTheory.Limits.pullback f (𝒰.f i)).OpenCover) [∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine ((𝒰' i).X j)] (h𝒰' : ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀), Q (CategoryTheory.Limits.pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f 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 : 𝒰.I₀), IsAffine (𝒰.X i)] (h𝒰 : ∀ (i : 𝒰.toPreZeroHypercover.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

theorem AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_of_openCover_source {Q : AffineTargetMorphismProperty} [Q.IsLocal] {X Y : Scheme} (f : X ⟶ Y) (𝒰 : X.OpenCover) [∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)] [IsAffine Y] (h𝒰 : ∀ (i j : 𝒰.I₀), Q (CategoryTheory.Limits.pullback.mapDesc (𝒰.f i) (𝒰.f j) f)) : Q.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.instIsZariskiLocalAtTargetDiagonalScheme (P : CategoryTheory.MorphismProperty Scheme) [IsZariskiLocalAtTarget P] : IsZariskiLocalAtTarget P.diagonal

instance AlgebraicGeometry.instIsZariskiLocalAtSourceDiagonalSchemeOfHasOfPostcompPropertyOfRespectsRightIsOpenImmersion (P : CategoryTheory.MorphismProperty Scheme) [P.HasOfPostcompProperty IsOpenImmersion] [P.RespectsRight IsOpenImmersion] [IsZariskiLocalAtSource P] : IsZariskiLocalAtSource P.diagonal

theorem AlgebraicGeometry.universally_isZariskiLocalAtTarget (P : CategoryTheory.MorphismProperty Scheme) (hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), TopologicalSpace.IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f) : IsZariskiLocalAtTarget P.universally

@[deprecated AlgebraicGeometry.universally_isZariskiLocalAtTarget (since := "2025-10-07")]

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

Alias of AlgebraicGeometry.universally_isZariskiLocalAtTarget.

theorem AlgebraicGeometry.universally_isZariskiLocalAtSource (P : CategoryTheory.MorphismProperty Scheme) [IsZariskiLocalAtSource P] : IsZariskiLocalAtSource P.universally

@[deprecated AlgebraicGeometry.universally_isZariskiLocalAtSource (since := "2025-10-07")]

theorem AlgebraicGeometry.universally_isLocalAtSource (P : CategoryTheory.MorphismProperty Scheme) [IsZariskiLocalAtSource P] : IsZariskiLocalAtSource P.universally

Alias of AlgebraicGeometry.universally_isZariskiLocalAtSource.

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

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

theorem AlgebraicGeometry.topologically_isStableUnderComposition (P : {α β : Type u} → [TopologicalSpace α] → [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} → [TopologicalSpace α] → [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} → [TopologicalSpace α] → [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_isZariskiLocalAtTarget (P : {α β : Type u} → [TopologicalSpace α] → [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 β), TopologicalSpace.IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f) : IsZariskiLocalAtTarget (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.

@[deprecated AlgebraicGeometry.topologically_isZariskiLocalAtTarget (since := "2025-10-07")]

theorem AlgebraicGeometry.topologically_isLocalAtTarget (P : {α β : Type u} → [TopologicalSpace α] → [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 β), TopologicalSpace.IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f) : IsZariskiLocalAtTarget (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => P)

Alias of AlgebraicGeometry.topologically_isZariskiLocalAtTarget.

---

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_isZariskiLocalAtTarget' (P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop) [(topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso] (hP : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → TopologicalSpace.Opens β), TopologicalSpace.IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))) : IsZariskiLocalAtTarget (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => P)

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

@[deprecated AlgebraicGeometry.topologically_isZariskiLocalAtTarget' (since := "2025-10-07")]

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

Alias of AlgebraicGeometry.topologically_isZariskiLocalAtTarget'.

---

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

theorem AlgebraicGeometry.topologically_isZariskiLocalAtSource (P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop) [(topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso] (hP₁ : ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y), Continuous f → ∀ (U : TopologicalSpace.Opens X), P f → P (f ∘ Subtype.val)) (hP₂ : ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y), Continuous f → ∀ {ι : Type u} (U : ι → TopologicalSpace.Opens X), TopologicalSpace.IsOpenCover U → (∀ (i : ι), P (f ∘ Subtype.val)) → P f) : IsZariskiLocalAtSource (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => P)

@[deprecated AlgebraicGeometry.topologically_isZariskiLocalAtSource (since := "2025-10-07")]

theorem AlgebraicGeometry.topologically_isLocalAtSource (P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop) [(topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso] (hP₁ : ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y), Continuous f → ∀ (U : TopologicalSpace.Opens X), P f → P (f ∘ Subtype.val)) (hP₂ : ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y), Continuous f → ∀ {ι : Type u} (U : ι → TopologicalSpace.Opens X), TopologicalSpace.IsOpenCover U → (∀ (i : ι), P (f ∘ Subtype.val)) → P f) : IsZariskiLocalAtSource (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => P)

Alias of AlgebraicGeometry.topologically_isZariskiLocalAtSource.

theorem AlgebraicGeometry.topologically_isZariskiLocalAtSource' (P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop) [(topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso] (hP : ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y) {ι : Type u} (U : ι → TopologicalSpace.Opens X), TopologicalSpace.IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P (f ∘ Subtype.val))) : IsZariskiLocalAtSource (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => P)

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

@[deprecated AlgebraicGeometry.topologically_isZariskiLocalAtSource' (since := "2025-10-07")]

theorem AlgebraicGeometry.topologically_isLocalAtSource' (P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop) [(topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso] (hP : ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y) {ι : Type u} (U : ι → TopologicalSpace.Opens X), TopologicalSpace.IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P (f ∘ Subtype.val))) : IsZariskiLocalAtSource (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => P)

Alias of AlgebraicGeometry.topologically_isZariskiLocalAtSource'.

---

A variant of topologically_isZariskiLocalAtSource 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.

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

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

@[deprecated AlgebraicGeometry.stalkwiseIsZariskiLocalAtTarget_of_respectsIso (since := "2025-10-07")]

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

Alias of AlgebraicGeometry.stalkwiseIsZariskiLocalAtTarget_of_respectsIso.

---

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

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

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

@[deprecated AlgebraicGeometry.stalkwise_isZariskiLocalAtSource_of_respectsIso (since := "2025-10-07")]

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

Alias of AlgebraicGeometry.stalkwise_isZariskiLocalAtSource_of_respectsIso.

---

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

theorem AlgebraicGeometry.stalkwise_SpecMap_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 φ) ⋯)

@[deprecated AlgebraicGeometry.stalkwise_SpecMap_iff (since := "2025-10-07")]

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 φ) ⋯)

Alias of AlgebraicGeometry.stalkwise_SpecMap_iff.

theorem AlgebraicGeometry.AffineTargetMorphismProperty.isStableUnderBaseChange_of_isStableUnderBaseChangeOnAffine_of_isZariskiLocalAtTarget (P : CategoryTheory.MorphismProperty Scheme) [IsZariskiLocalAtTarget 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.