# mathlib3documentation

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,
1. P respects isomorphisms.
2. If P holds for f : X ⟶ Y, then P holds for f ∣_ Y.basic_open r for any global section r.
3. 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
1. P respects isomorphisms.
2. If P holds for f : X ⟶ Y, then P holds for f ∣_ U for any U.
3. 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.

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

Equations
Instances for algebraic_geometry.affine_target_morphism_property
@[protected]

is_iso as a morphism_property.

Equations
@[protected]

is_iso as an affine_morphism_property.

Equations
@[protected, instance]
Equations

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

Equations
theorem algebraic_geometry.affine_target_morphism_property.respects_iso_mk (h₁ : {X Y Z : algebraic_geometry.Scheme} (e : X Y) (f : Y Z) [_inst_1 : , P f P (e.hom f)) (h₂ : {X Y Z : algebraic_geometry.Scheme} (e : Y Z) (f : X Y) [h : , P f P (f e.hom)) :

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

We say that P : affine_target_morphism_property is a local property if

1. P respects isomorphisms.
2. If P holds for f : X ⟶ Y, then P holds for f ∣_ Y.basic_open r for any global section r.
3. 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 (hP : P.is_local) {X Y : algebraic_geometry.Scheme} (f : X Y) (𝒰 : Y.open_cover) [ (i : 𝒰.J), ] (h𝒰 : (i : (𝒰.pullback_cover f).J), ) :
theorem algebraic_geometry.affine_target_morphism_property.is_local.affine_open_cover_tfae (hP : P.is_local) {X Y : algebraic_geometry.Scheme} (f : X Y) :
[, (𝒰 : Y.open_cover) [_inst_1 : (i : 𝒰.J), , (i : 𝒰.J), , (𝒰 : Y.open_cover) [_inst_2 : (i : 𝒰.J), (i : 𝒰.J), , {U : algebraic_geometry.Scheme} (g : U Y) [_inst_3 : [_inst_4 : , , {ι : Type u} (U : (hU : supr U = ) (hU' : (i : ι), , (i : ι), P (f ∣_ U i)].tfae
theorem algebraic_geometry.affine_target_morphism_property.is_local_of_open_cover_imply (hP : P.to_property.respects_iso) (H : {X Y : algebraic_geometry.Scheme} (f : X Y), ( (𝒰 : Y.open_cover) [_inst_1 : (i : 𝒰.J), , (i : 𝒰.J), {U : algebraic_geometry.Scheme} (g : U Y) [_inst_2 : [_inst_3 : , ) :

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

1. P respects isomorphisms.
2. If P holds for f : X ⟶ Y, then P holds for f ∣_ U for any U.
3. If P holds for f ∣_ U for an open cover U of Y, then P holds for f.
theorem algebraic_geometry.property_is_local_at_target.open_cover_tfae {X Y : algebraic_geometry.Scheme} (f : X Y) :
[P f, (𝒰 : Y.open_cover), (i : 𝒰.J), , (𝒰 : Y.open_cover) (i : 𝒰.J), , (U : , P (f ∣_ U), {U : algebraic_geometry.Scheme} (g : U Y) [_inst_1 : , , {ι : Type u} (U : (hU : supr U = ), (i : ι), P (f ∣_ U i)].tfae

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

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

Equations
theorem algebraic_geometry.diagonal_target_affine_locally_of_open_cover (hP : P.is_local) {X Y : algebraic_geometry.Scheme} (f : X Y) (𝒰 : Y.open_cover) [ (i : 𝒰.J), ] (𝒰' : Π (i : 𝒰.J), (𝒰.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)) :
theorem algebraic_geometry.affine_target_morphism_property.is_local.diagonal_affine_open_cover_tfae (hP : P.is_local) {X Y : algebraic_geometry.Scheme} (f : X Y) :
[, (𝒰 : Y.open_cover) [_inst_1 : (i : 𝒰.J), , (i : 𝒰.J), , (𝒰 : Y.open_cover) [_inst_2 : (i : 𝒰.J), (i : 𝒰.J), , {U : algebraic_geometry.Scheme} (g : U Y) [_inst_3 : [_inst_4 : , , (𝒰 : Y.open_cover) [_inst_5 : (i : 𝒰.J), (𝒰' : Π (i : 𝒰.J), (𝒰.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.universally_is_local_at_target (hP : {X Y : algebraic_geometry.Scheme} (f : X Y) (𝒰 : Y.open_cover), ( (i : 𝒰.J), P f) :
theorem algebraic_geometry.universally_is_local_at_target_of_morphism_restrict (hP₁ : P.respects_iso) (hP₂ : {X Y : algebraic_geometry.Scheme} (f : X Y) {ι : Type u} (U : , supr U = ( (i : ι), P (f ∣_ U i)) P f) :
def algebraic_geometry.morphism_property.topologically (P : Π {α β : Type u} [_inst_1 : [_inst_2 : , β) Prop) :

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

Equations