mathlib3 documentation

algebraic_geometry.morphisms.ring_hom_properties

Properties of morphisms from properties of ring homs. #

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

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]

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 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.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) :
theorem ring_hom.property_is_local.affine_locally_of_comp {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) (H : {R S T : Type u} [_inst_3 : comm_ring R] [_inst_4 : comm_ring S] [_inst_5 : comm_ring T] (f : R →+* S) (g : S →+* T), P (g.comp f) P g) {X Y Z : algebraic_geometry.Scheme} {f : X Y} {g : Y Z} (h : algebraic_geometry.affine_locally P (f g)) :