# mathlib3documentation

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,

• target_affine_locally (affine_and P): the preimage of an affine open U = Spec A is affine (= Spec B) and A ⟶ B satisfies P. (TODO)
• affine_locally P: For each pair of affine open U = Spec A ⊆ X and V = Spec B ⊆ f ⁻¹' U, the ring hom A ⟶ B satisfies P.

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)

theorem ring_hom.respects_iso.basic_open_iff {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (hP : ring_hom.respects_iso P) {X Y : algebraic_geometry.Scheme} (f : X Y)  :
theorem ring_hom.respects_iso.basic_open_iff_localization {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (hP : ring_hom.respects_iso P) {X Y : algebraic_geometry.Scheme} (f : X Y)  :
theorem ring_hom.respects_iso.of_restrict_morphism_restrict_iff {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (hP : ring_hom.respects_iso P) {X Y : algebraic_geometry.Scheme} (f : X Y) (e : V = .obj U) :
theorem ring_hom.stable_under_base_change.Γ_pullback_fst {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (hP' : ring_hom.respects_iso P) {X Y S : algebraic_geometry.Scheme} (f : X S) (g : Y S) (H : P ) :

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 : [_inst_2 : , (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.source_affine_locally_respects_iso {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (h₁ : ring_hom.respects_iso P) :
theorem algebraic_geometry.affine_locally_respects_iso {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (h : ring_hom.respects_iso P) :
theorem algebraic_geometry.affine_locally_iff_affine_opens_le {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (hP : ring_hom.respects_iso P) {X Y : algebraic_geometry.Scheme} (f : X Y) :
(U : (Y.affine_opens)) (V : (X.affine_opens)) (e : V.val U.val),
theorem algebraic_geometry.source_affine_locally_is_local {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (h₁ : ring_hom.respects_iso P)  :
theorem algebraic_geometry.source_affine_locally_of_source_open_cover_aux {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (h₁ : ring_hom.respects_iso P) {X Y : algebraic_geometry.Scheme} (f : X Y) (U : (X.affine_opens)) (hs : = ) (hs' : (r : s), P (algebraic_geometry.Scheme.Γ.map (X.of_restrict _ f).op)) :
theorem algebraic_geometry.is_open_immersion_comp_of_source_affine_locally {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (h₁ : ring_hom.respects_iso P) {X Y Z : algebraic_geometry.Scheme} (f : X Y) (g : Y Z)  :
theorem ring_hom.property_is_local.source_affine_locally_of_source_open_cover {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (hP : ring_hom.property_is_local P) {X Y : algebraic_geometry.Scheme} (f : X Y) (𝒰 : X.open_cover) [ (i : 𝒰.J), ] (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 : [_inst_2 : , (R →+* S) Prop} (hP : ring_hom.property_is_local P) {X Y : algebraic_geometry.Scheme} (f : X Y) :
[, (𝒰 : X.open_cover) [_inst_4 : (i : 𝒰.J), , (i : 𝒰.J), P (algebraic_geometry.Scheme.Γ.map (𝒰.map i f).op), (𝒰 : X.open_cover) [_inst_5 : (i : 𝒰.J), (i : 𝒰.J), P (algebraic_geometry.Scheme.Γ.map (𝒰.map i f).op), {U : algebraic_geometry.Scheme} (g : U X) [_inst_6 : [_inst_7 : , P (algebraic_geometry.Scheme.Γ.map (g f).op)].tfae
theorem ring_hom.property_is_local.open_cover_tfae {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (hP : ring_hom.property_is_local P) {X Y : algebraic_geometry.Scheme} (f : X Y) :
[, (𝒰 : X.open_cover), (i : 𝒰.J), (𝒰.map i f), (𝒰 : X.open_cover) (i : 𝒰.J), (𝒰.map i f), {U : algebraic_geometry.Scheme} (g : U X) [_inst_4 : , .tfae
theorem ring_hom.property_is_local.source_affine_locally_comp_of_is_open_immersion {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (hP : ring_hom.property_is_local P) {X Y Z : algebraic_geometry.Scheme} (f : X Y) (g : Y Z)  :
theorem ring_hom.property_is_local.source_affine_open_cover_iff {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (hP : ring_hom.property_is_local P) {X Y : algebraic_geometry.Scheme} (f : X Y) (𝒰 : X.open_cover) [ (i : 𝒰.J), ] :
(i : 𝒰.J), P (algebraic_geometry.Scheme.Γ.map (𝒰.map i f).op)
theorem ring_hom.property_is_local.is_local_source_affine_locally {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (hP : ring_hom.property_is_local P) :
theorem ring_hom.property_is_local.is_local_affine_locally {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (hP : ring_hom.property_is_local P) :
theorem ring_hom.property_is_local.affine_open_cover_iff {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (hP : ring_hom.property_is_local P) {X Y : algebraic_geometry.Scheme} (f : X Y) (𝒰 : Y.open_cover) [ (i : 𝒰.J), ] (𝒰' : Π (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)] :
(i : (𝒰.pullback_cover f).J) (j : (𝒰' i).J), P
theorem ring_hom.property_is_local.source_open_cover_iff {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (hP : ring_hom.property_is_local P) {X Y : algebraic_geometry.Scheme} (f : X Y) (𝒰 : X.open_cover) :
(i : 𝒰.J), (𝒰.map i f)
theorem ring_hom.property_is_local.affine_locally_of_is_open_immersion {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (hP : ring_hom.property_is_local P) {X Y : algebraic_geometry.Scheme} (f : X Y)  :
theorem ring_hom.property_is_local.affine_locally_of_comp {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (hP : ring_hom.property_is_local P) (H : {R S T : Type u} [_inst_3 : [_inst_4 : [_inst_5 : (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 : (f g)) :
theorem ring_hom.property_is_local.affine_locally_stable_under_composition {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (hP : ring_hom.property_is_local P) :