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 #

  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.
  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 #

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

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

Equations

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.

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.

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

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

Equations