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 openU = Spec Ais affine (= Spec B) andA ⟶ BsatisfiesP. (TODO)affine_locally P: For each pair of affine openU = Spec A ⊆ XandV = Spec B ⊆ f ⁻¹' U, the ring homA ⟶ BsatisfiesP.
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 : comm_ring R] [_inst_2 : comm_ring S], (R →+* S) → Prop}
(hP : ring_hom.respects_iso P)
{X Y : algebraic_geometry.Scheme}
[algebraic_geometry.is_affine X]
[algebraic_geometry.is_affine Y]
(f : X ⟶ Y)
(r : ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op ⊤))) :
P (algebraic_geometry.Scheme.Γ.map (f ∣_ Y.basic_open r).op) ↔ P (is_localization.away.map ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op (Y.basic_open r))) ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op (X.basic_open (⇑(algebraic_geometry.Scheme.Γ.map f.op) r)))) (algebraic_geometry.Scheme.Γ.map f.op) r)
theorem
ring_hom.respects_iso.basic_open_iff_localization
{P : Π {R S : Type u} [_inst_1 : comm_ring R] [_inst_2 : comm_ring S], (R →+* S) → Prop}
(hP : ring_hom.respects_iso P)
{X Y : algebraic_geometry.Scheme}
[algebraic_geometry.is_affine X]
[algebraic_geometry.is_affine Y]
(f : X ⟶ Y)
(r : ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op ⊤))) :
P (algebraic_geometry.Scheme.Γ.map (f ∣_ Y.basic_open r).op) ↔ P (localization.away_map (algebraic_geometry.Scheme.Γ.map f.op) r)
theorem
ring_hom.respects_iso.of_restrict_morphism_restrict_iff
{P : Π {R S : Type u} [_inst_1 : comm_ring R] [_inst_2 : comm_ring S], (R →+* S) → Prop}
(hP : ring_hom.respects_iso P)
{X Y : algebraic_geometry.Scheme}
[algebraic_geometry.is_affine Y]
(f : X ⟶ Y)
(r : ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op ⊤)))
(U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier))
(hU : algebraic_geometry.is_affine_open U)
{V : topological_space.opens ↥↑((X.restrict _).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace)}
(e : V = (topological_space.opens.map (X.of_restrict _).val.base).obj U) :
P (algebraic_geometry.Scheme.Γ.map ((X.restrict _).of_restrict _ ≫ f ∣_ Y.basic_open r).op) ↔ P (localization.away_map (algebraic_geometry.Scheme.Γ.map (X.of_restrict _ ≫ f).op) r)
theorem
ring_hom.stable_under_base_change.Γ_pullback_fst
{P : Π {R S : Type u} [_inst_1 : comm_ring R] [_inst_2 : comm_ring S], (R →+* S) → Prop}
(hP : ring_hom.stable_under_base_change P)
(hP' : ring_hom.respects_iso P)
{X Y S : algebraic_geometry.Scheme}
[algebraic_geometry.is_affine X]
[algebraic_geometry.is_affine Y]
[algebraic_geometry.is_affine S]
(f : X ⟶ S)
(g : Y ⟶ S)
(H : P (algebraic_geometry.Scheme.Γ.map g.op)) :
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
- algebraic_geometry.source_affine_locally P = λ (X Y : algebraic_geometry.Scheme) (f : X ⟶ Y) (hY : algebraic_geometry.is_affine Y), ∀ (U : ↥(X.affine_opens)), P (algebraic_geometry.Scheme.Γ.map (X.of_restrict _ ≫ f).op)
@[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.source_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
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
algebraic_geometry.affine_locally_iff_affine_opens_le
{P : Π {R S : Type u} [_inst_1 : comm_ring R] [_inst_2 : comm_ring S], (R →+* S) → Prop}
(hP : ring_hom.respects_iso P)
{X Y : algebraic_geometry.Scheme}
(f : X ⟶ Y) :
algebraic_geometry.affine_locally P f ↔ ∀ (U : ↥(Y.affine_opens)) (V : ↥(X.affine_opens)) (e : V.val ≤ (topological_space.opens.map f.val.base).obj U.val), P (algebraic_geometry.Scheme.hom.app_le f e)
theorem
algebraic_geometry.Scheme_restrict_basic_open_of_localization_preserves
{P : Π {R S : Type u} [_inst_1 : comm_ring R] [_inst_2 : comm_ring S], (R →+* S) → Prop}
(h₁ : ring_hom.respects_iso P)
(h₂ : ring_hom.localization_preserves P)
{X Y : algebraic_geometry.Scheme}
[algebraic_geometry.is_affine Y]
(f : X ⟶ Y)
(r : ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op ⊤)))
(H : algebraic_geometry.source_affine_locally P f)
(U : ↥((X.restrict _).affine_opens)) :
P (algebraic_geometry.Scheme.Γ.map ((X.restrict _).of_restrict _ ≫ f ∣_ Y.basic_open r).op)
theorem
algebraic_geometry.source_affine_locally_is_local
{P : Π {R S : Type u} [_inst_1 : comm_ring R] [_inst_2 : comm_ring S], (R →+* S) → Prop}
(h₁ : ring_hom.respects_iso P)
(h₂ : ring_hom.localization_preserves P)
(h₃ : ring_hom.of_localization_span P) :
theorem
algebraic_geometry.source_affine_locally_of_source_open_cover_aux
{P : Π {R S : Type u} [_inst_1 : comm_ring R] [_inst_2 : comm_ring S], (R →+* S) → Prop}
(h₁ : ring_hom.respects_iso P)
(h₃ : ring_hom.of_localization_span_target P)
{X Y : algebraic_geometry.Scheme}
(f : X ⟶ Y)
(U : ↥(X.affine_opens))
(s : set ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U.val)))
(hs : ideal.span s = ⊤)
(hs' : ∀ (r : ↥s), P (algebraic_geometry.Scheme.Γ.map (X.of_restrict _ ≫ f).op)) :
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 : comm_ring R] [_inst_2 : comm_ring S], (R →+* S) → Prop}
(h₁ : ring_hom.respects_iso P)
{X Y Z : algebraic_geometry.Scheme}
[algebraic_geometry.is_affine X]
[algebraic_geometry.is_affine Z]
(f : X ⟶ Y)
[algebraic_geometry.is_open_immersion f]
(g : Y ⟶ Z)
(h₂ : algebraic_geometry.source_affine_locally P g) :
P (algebraic_geometry.Scheme.Γ.map (f ≫ g).op)
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.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), ∀ (i : 𝒰.J), algebraic_geometry.source_affine_locally P (𝒰.map i ≫ f), ∀ (𝒰 : X.open_cover) (i : 𝒰.J), algebraic_geometry.source_affine_locally P (𝒰.map i ≫ f), ∀ {U : algebraic_geometry.Scheme} (g : U ⟶ X) [_inst_4 : algebraic_geometry.is_open_immersion g], algebraic_geometry.source_affine_locally P (g ≫ f)].tfae
theorem
ring_hom.property_is_local.source_affine_locally_comp_of_is_open_immersion
{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 Z : algebraic_geometry.Scheme}
[algebraic_geometry.is_affine Z]
(f : X ⟶ Y)
(g : Y ⟶ Z)
[algebraic_geometry.is_open_immersion f]
(H : algebraic_geometry.source_affine_locally P g) :
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)] :
algebraic_geometry.source_affine_locally P f ↔ ∀ (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 : comm_ring R] [_inst_2 : comm_ring S], (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 : comm_ring R] [_inst_2 : comm_ring S], (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 : 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)] :
algebraic_geometry.affine_locally P f ↔ ∀ (i : (𝒰.pullback_cover f).J) (j : (𝒰' i).J), P (algebraic_geometry.Scheme.Γ.map ((𝒰' i).map j ≫ category_theory.limits.pullback.snd).op)
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) :
algebraic_geometry.affine_locally P f ↔ ∀ (i : 𝒰.J), algebraic_geometry.affine_locally P (𝒰.map i ≫ f)
theorem
ring_hom.property_is_local.affine_locally_of_is_open_immersion
{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)
[hf : algebraic_geometry.is_open_immersion f] :
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)) :
theorem
ring_hom.property_is_local.affine_locally_stable_under_composition
{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) :