mathlib3 documentation

algebraic_geometry.morphisms.basic

Properties of morphisms between Schemes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We provide the basic framework for talking about properties of morphisms between Schemes.

A morphism_property Scheme is a predicate on morphisms between schemes, and an affine_target_morphism_property is a predicate on morphisms into affine schemes. Given a P : affine_target_morphism_property, we may construct a morphism_property called target_affine_locally P that holds for f : X ⟶ Y whenever P holds for the restriction of f on every affine open subset of Y.

Main definitions #

algebraic_geometry.affine_target_morphism_property.is_local: We say that P.is_local if P satisfies the assumptions of the affine communication lemma (algebraic_geometry.of_affine_open_cover). That is,

P respects isomorphisms.
If P holds for f : X ⟶ Y, then P holds for f ∣_ Y.basic_open r for any global section r.
If P holds for f ∣_ Y.basic_open r for all r in a spanning set of the global sections, then P holds for f.

algebraic_geometry.property_is_local_at_target: We say that property_is_local_at_target P for P : morphism_property Scheme if

P respects isomorphisms.
If P holds for f : X ⟶ Y, then P holds for f ∣_ U for any U.
If P holds for f ∣_ U for an open cover U of Y, then P holds for f.

Main results #

algebraic_geometry.affine_target_morphism_property.is_local.affine_open_cover_tfae: If P.is_local, then target_affine_locally P f iff there exists an affine cover { Uᵢ } of Y such that P holds for f ∣_ Uᵢ.
algebraic_geometry.affine_target_morphism_property.is_local_of_open_cover_imply: If the existance of an affine cover { Uᵢ } of Y such that P holds for f ∣_ Uᵢ implies target_affine_locally P f, then P.is_local.
algebraic_geometry.affine_target_morphism_property.is_local.affine_target_iff: If Y is affine and f : X ⟶ Y, then target_affine_locally P f ↔ P f provided P.is_local.
algebraic_geometry.affine_target_morphism_property.is_local.target_affine_locally_is_local : If P.is_local, then property_is_local_at_target (target_affine_locally P).
algebraic_geometry.property_is_local_at_target.open_cover_tfae: If property_is_local_at_target P, then P f iff there exists an open cover { Uᵢ } of Y such that P holds for f ∣_ Uᵢ.

These results should not be used directly, and should be ported to each property that is local.

def algebraic_geometry.affine_target_morphism_property :

Type (u_1+1)

An affine_target_morphism_property is a class of morphisms from an arbitrary scheme into an affine scheme.

Equations

algebraic_geometry.affine_target_morphism_property = Π ⦃X Y : algebraic_geometry.Scheme⦄, (X ⟶ Y) → Π [_inst_1 : algebraic_geometry.is_affine Y], Prop

Instances for algebraic_geometry.affine_target_morphism_property

algebraic_geometry.affine_target_morphism_property.inhabited

@[protected]

def algebraic_geometry.Scheme.is_iso :

category_theory.morphism_property algebraic_geometry.Scheme

is_iso as a morphism_property.

Equations

algebraic_geometry.Scheme.is_iso = category_theory.is_iso

@[protected]

def algebraic_geometry.Scheme.affine_target_is_iso :

algebraic_geometry.affine_target_morphism_property

is_iso as an affine_morphism_property.

Equations

algebraic_geometry.Scheme.affine_target_is_iso = λ (X Y : algebraic_geometry.Scheme) (f : X ⟶ Y) (H : algebraic_geometry.is_affine Y), category_theory.is_iso f

@[protected, instance]

def algebraic_geometry.affine_target_morphism_property.inhabited :

inhabited algebraic_geometry.affine_target_morphism_property

Equations

algebraic_geometry.affine_target_morphism_property.inhabited = {default := algebraic_geometry.Scheme.affine_target_is_iso}

def algebraic_geometry.affine_target_morphism_property.to_property (P : algebraic_geometry.affine_target_morphism_property) :

category_theory.morphism_property algebraic_geometry.Scheme

A affine_target_morphism_property can be extended to a morphism_property such that it never holds when the target is not affine

Equations

P.to_property = λ (X Y : algebraic_geometry.Scheme) (f : X ⟶ Y), ∃ (h : algebraic_geometry.is_affine Y), P f

theorem algebraic_geometry.affine_target_morphism_property.to_property_apply (P : algebraic_geometry.affine_target_morphism_property) {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [algebraic_geometry.is_affine Y] :

P.to_property f ↔ P f

theorem algebraic_geometry.affine_cancel_left_is_iso {P : algebraic_geometry.affine_target_morphism_property} (hP : P.to_property.respects_iso) {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.is_iso f] [algebraic_geometry.is_affine Z] :

P (f ≫ g) ↔ P g

theorem algebraic_geometry.affine_cancel_right_is_iso {P : algebraic_geometry.affine_target_morphism_property} (hP : P.to_property.respects_iso) {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.is_iso g] [algebraic_geometry.is_affine Z] [algebraic_geometry.is_affine Y] :

P (f ≫ g) ↔ P f

theorem algebraic_geometry.affine_target_morphism_property.respects_iso_mk {P : algebraic_geometry.affine_target_morphism_property} (h₁ : ∀ {X Y Z : algebraic_geometry.Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [_inst_1 : algebraic_geometry.is_affine Z], P f → P (e.hom ≫ f)) (h₂ : ∀ {X Y Z : algebraic_geometry.Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [h : algebraic_geometry.is_affine Y], P f → P (f ≫ e.hom)) :

P.to_property.respects_iso

def algebraic_geometry.target_affine_locally (P : algebraic_geometry.affine_target_morphism_property) :

category_theory.morphism_property algebraic_geometry.Scheme

For a P : affine_target_morphism_property, target_affine_locally P holds for f : X ⟶ Y whenever P holds for the restriction of f on every affine open subset of Y.

Equations

algebraic_geometry.target_affine_locally P = λ {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y), ∀ (U : ↥(Y.affine_opens)), P (f ∣_ ↑U)

theorem algebraic_geometry.is_affine_open.map_is_iso {X Y : algebraic_geometry.Scheme} {U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) (f : X ⟶ Y) [category_theory.is_iso f] :

algebraic_geometry.is_affine_open ((topological_space.opens.map f.val.base).obj U)

theorem algebraic_geometry.target_affine_locally_respects_iso {P : algebraic_geometry.affine_target_morphism_property} (hP : P.to_property.respects_iso) :

(algebraic_geometry.target_affine_locally P).respects_iso

structure algebraic_geometry.affine_target_morphism_property.is_local (P : algebraic_geometry.affine_target_morphism_property) :

Prop

respects_iso : P.to_property.respects_iso
to_basic_open : ∀ {X Y : algebraic_geometry.Scheme} [_inst_1 : algebraic_geometry.is_affine Y] (f : X ⟶ Y) (r : ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op ⊤))), P f → P (f ∣_ Y.basic_open r)
of_basic_open_cover : ∀ {X Y : algebraic_geometry.Scheme} [_inst_1 : algebraic_geometry.is_affine Y] (f : X ⟶ Y) (s : finset ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op ⊤))), ideal.span ↑s = ⊤ → (∀ (r : ↥s), P (f ∣_ Y.basic_open r.val)) → P f

We say that P : affine_target_morphism_property is a local property if

P respects isomorphisms.
If P holds for f : X ⟶ Y, then P holds for f ∣_ Y.basic_open r for any global section r.
If P holds for f ∣_ Y.basic_open r for all r in a spanning set of the global sections, then P holds for f.

theorem algebraic_geometry.target_affine_locally_of_open_cover {P : algebraic_geometry.affine_target_morphism_property} (hP : P.is_local) {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.open_cover) [∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)] (h𝒰 : ∀ (i : (𝒰.pullback_cover f).J), P category_theory.limits.pullback.snd) :

algebraic_geometry.target_affine_locally P f

theorem algebraic_geometry.affine_target_morphism_property.is_local.affine_open_cover_tfae {P : algebraic_geometry.affine_target_morphism_property} (hP : P.is_local) {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) :

[algebraic_geometry.target_affine_locally P f, ∃ (𝒰 : Y.open_cover) [_inst_1 : ∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)], ∀ (i : 𝒰.J), P category_theory.limits.pullback.snd, ∀ (𝒰 : Y.open_cover) [_inst_2 : ∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)] (i : 𝒰.J), P category_theory.limits.pullback.snd, ∀ {U : algebraic_geometry.Scheme} (g : U ⟶ Y) [_inst_3 : algebraic_geometry.is_affine U] [_inst_4 : algebraic_geometry.is_open_immersion g], P category_theory.limits.pullback.snd, ∃ {ι : Type u} (U : ι → topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (hU : supr U = ⊤) (hU' : ∀ (i : ι), algebraic_geometry.is_affine_open (U i)), ∀ (i : ι), P (f ∣_ U i)].tfae

theorem algebraic_geometry.affine_target_morphism_property.is_local_of_open_cover_imply (P : algebraic_geometry.affine_target_morphism_property) (hP : P.to_property.respects_iso) (H : ∀ {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y), (∃ (𝒰 : Y.open_cover) [_inst_1 : ∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)], ∀ (i : 𝒰.J), P category_theory.limits.pullback.snd) → ∀ {U : algebraic_geometry.Scheme} (g : U ⟶ Y) [_inst_2 : algebraic_geometry.is_affine U] [_inst_3 : algebraic_geometry.is_open_immersion g], P category_theory.limits.pullback.snd) :

theorem algebraic_geometry.affine_target_morphism_property.is_local.affine_open_cover_iff {P : algebraic_geometry.affine_target_morphism_property} (hP : P.is_local) {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.open_cover) [h𝒰 : ∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)] :

algebraic_geometry.target_affine_locally P f ↔ ∀ (i : 𝒰.J), P category_theory.limits.pullback.snd

theorem algebraic_geometry.affine_target_morphism_property.is_local.affine_target_iff {P : algebraic_geometry.affine_target_morphism_property} (hP : P.is_local) {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [algebraic_geometry.is_affine Y] :

algebraic_geometry.target_affine_locally P f ↔ P f

structure algebraic_geometry.property_is_local_at_target (P : category_theory.morphism_property algebraic_geometry.Scheme) :

Prop

respects_iso : P.respects_iso
restrict : ∀ {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), P f → P (f ∣_ U)
of_open_cover : ∀ {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.open_cover), (∀ (i : 𝒰.J), P category_theory.limits.pullback.snd) → P f

We say that P : morphism_property Scheme is local at the target if

P respects isomorphisms.
If P holds for f : X ⟶ Y, then P holds for f ∣_ U for any U.
If P holds for f ∣_ U for an open cover U of Y, then P holds for f.

theorem algebraic_geometry.affine_target_morphism_property.is_local.target_affine_locally_is_local {P : algebraic_geometry.affine_target_morphism_property} (hP : P.is_local) :

algebraic_geometry.property_is_local_at_target (algebraic_geometry.target_affine_locally P)

theorem algebraic_geometry.property_is_local_at_target.open_cover_tfae {P : category_theory.morphism_property algebraic_geometry.Scheme} (hP : algebraic_geometry.property_is_local_at_target P) {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) :

[P f, ∃ (𝒰 : Y.open_cover), ∀ (i : 𝒰.J), P category_theory.limits.pullback.snd, ∀ (𝒰 : Y.open_cover) (i : 𝒰.J), P category_theory.limits.pullback.snd, ∀ (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), P (f ∣_ U), ∀ {U : algebraic_geometry.Scheme} (g : U ⟶ Y) [_inst_1 : algebraic_geometry.is_open_immersion g], P category_theory.limits.pullback.snd, ∃ {ι : Type u} (U : ι → topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (hU : supr U = ⊤), ∀ (i : ι), P (f ∣_ U i)].tfae

theorem algebraic_geometry.property_is_local_at_target.open_cover_iff {P : category_theory.morphism_property algebraic_geometry.Scheme} (hP : algebraic_geometry.property_is_local_at_target P) {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.open_cover) :

P f ↔ ∀ (i : 𝒰.J), P category_theory.limits.pullback.snd

def algebraic_geometry.affine_target_morphism_property.stable_under_base_change (P : algebraic_geometry.affine_target_morphism_property) :

Prop

A P : affine_target_morphism_property is stable under base change if P holds for Y ⟶ S implies that P holds for X ×ₛ Y ⟶ X with X and S affine schemes.

Equations

P.stable_under_base_change = ∀ ⦃X Y S : algebraic_geometry.Scheme⦄ [_inst_1 : algebraic_geometry.is_affine S] [_inst_2 : algebraic_geometry.is_affine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P category_theory.limits.pullback.fst

theorem algebraic_geometry.affine_target_morphism_property.is_local.target_affine_locally_pullback_fst_of_right_of_stable_under_base_change {P : algebraic_geometry.affine_target_morphism_property} (hP : P.is_local) (hP' : P.stable_under_base_change) {X Y S : algebraic_geometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [algebraic_geometry.is_affine S] (H : P g) :

algebraic_geometry.target_affine_locally P category_theory.limits.pullback.fst

theorem algebraic_geometry.affine_target_morphism_property.is_local.stable_under_base_change {P : algebraic_geometry.affine_target_morphism_property} (hP : P.is_local) (hP' : P.stable_under_base_change) :

(algebraic_geometry.target_affine_locally P).stable_under_base_change

def algebraic_geometry.affine_target_morphism_property.diagonal (P : algebraic_geometry.affine_target_morphism_property) :

algebraic_geometry.affine_target_morphism_property

The affine_target_morphism_property associated to (target_affine_locally P).diagonal. See diagonal_target_affine_locally_eq_target_affine_locally.

Equations

P.diagonal = λ (X Y : algebraic_geometry.Scheme) (f : X ⟶ Y) (hf : algebraic_geometry.is_affine Y), ∀ {U₁ U₂ : algebraic_geometry.Scheme} (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [_inst_1 : algebraic_geometry.is_affine U₁] [_inst_2 : algebraic_geometry.is_affine U₂] [_inst_3 : algebraic_geometry.is_open_immersion f₁] [_inst_4 : algebraic_geometry.is_open_immersion f₂], P (category_theory.limits.pullback.map_desc f₁ f₂ f)

theorem algebraic_geometry.affine_target_morphism_property.diagonal_respects_iso (P : algebraic_geometry.affine_target_morphism_property) (hP : P.to_property.respects_iso) :

P.diagonal.to_property.respects_iso

theorem algebraic_geometry.diagonal_target_affine_locally_of_open_cover (P : algebraic_geometry.affine_target_morphism_property) (hP : P.is_local) {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.open_cover) [∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)] (𝒰' : Π (i : 𝒰.J), (category_theory.limits.pullback f (𝒰.map i)).open_cover) [∀ (i : 𝒰.J) (j : (𝒰' i).J), algebraic_geometry.is_affine ((𝒰' i).obj j)] (h𝒰' : ∀ (i : 𝒰.J) (j k : (𝒰' i).J), P (category_theory.limits.pullback.map_desc ((𝒰' i).map j) ((𝒰' i).map k) category_theory.limits.pullback.snd)) :

(algebraic_geometry.target_affine_locally P).diagonal f

theorem algebraic_geometry.affine_target_morphism_property.diagonal_of_target_affine_locally (P : algebraic_geometry.affine_target_morphism_property) (hP : P.is_local) {X Y U : algebraic_geometry.Scheme} (f : X ⟶ Y) (g : U ⟶ Y) [algebraic_geometry.is_affine U] [algebraic_geometry.is_open_immersion g] (H : (algebraic_geometry.target_affine_locally P).diagonal f) :

P.diagonal category_theory.limits.pullback.snd

theorem algebraic_geometry.affine_target_morphism_property.is_local.diagonal_affine_open_cover_tfae {P : algebraic_geometry.affine_target_morphism_property} (hP : P.is_local) {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) :

[(algebraic_geometry.target_affine_locally P).diagonal f, ∃ (𝒰 : Y.open_cover) [_inst_1 : ∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)], ∀ (i : 𝒰.J), P.diagonal category_theory.limits.pullback.snd, ∀ (𝒰 : Y.open_cover) [_inst_2 : ∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)] (i : 𝒰.J), P.diagonal category_theory.limits.pullback.snd, ∀ {U : algebraic_geometry.Scheme} (g : U ⟶ Y) [_inst_3 : algebraic_geometry.is_affine U] [_inst_4 : algebraic_geometry.is_open_immersion g], P.diagonal category_theory.limits.pullback.snd, ∃ (𝒰 : Y.open_cover) [_inst_5 : ∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)] (𝒰' : Π (i : 𝒰.J), (category_theory.limits.pullback f (𝒰.map i)).open_cover) [_inst_6 : ∀ (i : 𝒰.J) (j : (𝒰' i).J), algebraic_geometry.is_affine ((𝒰' i).obj j)], ∀ (i : 𝒰.J) (j k : (𝒰' i).J), P (category_theory.limits.pullback.map_desc ((𝒰' i).map j) ((𝒰' i).map k) category_theory.limits.pullback.snd)].tfae

theorem algebraic_geometry.affine_target_morphism_property.is_local.diagonal {P : algebraic_geometry.affine_target_morphism_property} (hP : P.is_local) :

P.diagonal.is_local

theorem algebraic_geometry.diagonal_target_affine_locally_eq_target_affine_locally (P : algebraic_geometry.affine_target_morphism_property) (hP : P.is_local) :

(algebraic_geometry.target_affine_locally P).diagonal = algebraic_geometry.target_affine_locally P.diagonal

theorem algebraic_geometry.universally_is_local_at_target (P : category_theory.morphism_property algebraic_geometry.Scheme) (hP : ∀ {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.open_cover), (∀ (i : 𝒰.J), P category_theory.limits.pullback.snd) → P f) :

algebraic_geometry.property_is_local_at_target P.universally

theorem algebraic_geometry.universally_is_local_at_target_of_morphism_restrict (P : category_theory.morphism_property algebraic_geometry.Scheme) (hP₁ : P.respects_iso) (hP₂ : ∀ {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), supr U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f) :

algebraic_geometry.property_is_local_at_target P.universally

def algebraic_geometry.morphism_property.topologically (P : Π {α β : Type u} [_inst_1 : topological_space α] [_inst_2 : topological_space β], (α → β) → Prop) :

category_theory.morphism_property algebraic_geometry.Scheme

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

Equations

algebraic_geometry.morphism_property.topologically P = λ (X Y : algebraic_geometry.Scheme) (f : X ⟶ Y), P ⇑(f.val.base)