mathlib documentation

algebraic_geometry.morphisms.ring_hom_properties

Properties of morphisms from properties of ring homs. #

We provide the basic framework for talking about properties of morphisms that come from properties of ring homs. For P a property of ring homs, we have two ways of defining a property of scheme morphisms:

Let f : X ⟶ Y,

For these notions to be well defined, we require P be a sufficient local property. For the former, P should be local on the source (ring_hom.respects_iso P, ring_hom.localization_preserves P, ring_hom.of_localization_span), and target_affine_locally (affine_and P) will be local on the target. (TODO)

For the latter P should be local on the target (ring_hom.property_is_local P), and affine_locally P will be local on both the source and the target.

Further more, these properties are stable under compositions (resp. base change) if P is. (TODO)

def algebraic_geometry.source_affine_locally (P : Π {R S : Type u} [_inst_1 : comm_ring R] [_inst_2 : comm_ring S], (R →+* S) → Prop) :

For P a property of ring homomorphisms, source_affine_locally P holds for f : X ⟶ Y whenever P holds for the restriction of f on every affine open subset of X.

Equations
@[reducible]
def algebraic_geometry.affine_locally (P : Π {R S : Type u} [_inst_1 : comm_ring R] [_inst_2 : comm_ring S], (R →+* S) → Prop) :

For P a property of ring homomorphisms, affine_locally P holds for f : X ⟶ Y if for each affine open U = Spec A ⊆ Y and V = Spec B ⊆ f ⁻¹' U, the ring hom A ⟶ B satisfies P. Also see affine_locally_iff_affine_opens_le.

theorem algebraic_geometry.affine_locally_respects_iso {P : Π {R S : Type u} [_inst_1 : comm_ring R] [_inst_2 : comm_ring S], (R →+* S) → Prop} (h : ring_hom.respects_iso P) :
theorem ring_hom.property_is_local.source_affine_locally_of_source_open_cover {P : Π {R S : Type u} [_inst_1 : comm_ring R] [_inst_2 : comm_ring S], (R →+* S) → Prop} (hP : ring_hom.property_is_local P) {X Y : algebraic_geometry.Scheme} (f : X Y) [algebraic_geometry.is_affine Y] (𝒰 : X.open_cover) [∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)] (H : ∀ (i : 𝒰.J), P (algebraic_geometry.Scheme.Γ.map (𝒰.map i f).op)) :
theorem ring_hom.property_is_local.affine_open_cover_tfae {P : Π {R S : Type u} [_inst_1 : comm_ring R] [_inst_2 : comm_ring S], (R →+* S) → Prop} (hP : ring_hom.property_is_local P) {X Y : algebraic_geometry.Scheme} [algebraic_geometry.is_affine Y] (f : X Y) :
[algebraic_geometry.source_affine_locally P f, ∃ (𝒰 : X.open_cover) [_inst_4 : ∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)], ∀ (i : 𝒰.J), P (algebraic_geometry.Scheme.Γ.map (𝒰.map i f).op), ∀ (𝒰 : X.open_cover) [_inst_5 : ∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)] (i : 𝒰.J), P (algebraic_geometry.Scheme.Γ.map (𝒰.map i f).op), ∀ {U : algebraic_geometry.Scheme} (g : U X) [_inst_6 : algebraic_geometry.is_affine U] [_inst_7 : algebraic_geometry.is_open_immersion g], P (algebraic_geometry.Scheme.Γ.map (g f).op)].tfae
theorem ring_hom.property_is_local.source_affine_open_cover_iff {P : Π {R S : Type u} [_inst_1 : comm_ring R] [_inst_2 : comm_ring S], (R →+* S) → Prop} (hP : ring_hom.property_is_local P) {X Y : algebraic_geometry.Scheme} (f : X Y) [algebraic_geometry.is_affine Y] (𝒰 : X.open_cover) [∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)] :
theorem ring_hom.property_is_local.affine_open_cover_iff {P : Π {R S : Type u} [_inst_1 : comm_ring R] [_inst_2 : comm_ring S], (R →+* S) → Prop} (hP : ring_hom.property_is_local P) {X Y : algebraic_geometry.Scheme} (f : X Y) (𝒰 : Y.open_cover) [∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)] (𝒰' : Π (i : (𝒰.pullback_cover f).J), ((𝒰.pullback_cover f).obj i).open_cover) [∀ (i : (𝒰.pullback_cover f).J) (j : (𝒰' i).J), algebraic_geometry.is_affine ((𝒰' i).obj j)] :
theorem ring_hom.property_is_local.source_open_cover_iff {P : Π {R S : Type u} [_inst_1 : comm_ring R] [_inst_2 : comm_ring S], (R →+* S) → Prop} (hP : ring_hom.property_is_local P) {X Y : algebraic_geometry.Scheme} (f : X Y) (𝒰 : X.open_cover) :