Open immersions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
A morphism is an open immersions if the underlying map of spaces is an open embedding
f : X ⟶ U ⊆ Y, and the sheaf map Y(V) ⟶ f _* X(V) is an iso for each V ⊆ U.
Most of the theories are developed in algebraic_geometry/open_immersion, and we provide the
remaining theorems analogous to other lemmas in algebraic_geometry/morphisms/*.
theorem
algebraic_geometry.is_open_immersion_iff_stalk
{X Y : algebraic_geometry.Scheme}
{f : X ⟶ Y} :
theorem
algebraic_geometry.is_open_immersion.open_cover_tfae
{X Y : algebraic_geometry.Scheme}
(f : X ⟶ Y) :
[algebraic_geometry.is_open_immersion f, ∃ (𝒰 : Y.open_cover), ∀ (i : 𝒰.J), algebraic_geometry.is_open_immersion category_theory.limits.pullback.snd, ∀ (𝒰 : Y.open_cover) (i : 𝒰.J), algebraic_geometry.is_open_immersion category_theory.limits.pullback.snd, ∀ (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), algebraic_geometry.is_open_immersion (f ∣_ U), ∀ {U : algebraic_geometry.Scheme} (g : U ⟶ Y) [_inst_1 : algebraic_geometry.is_open_immersion g], algebraic_geometry.is_open_immersion category_theory.limits.pullback.snd, ∃ {ι : Type u} (U : ι → topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (hU : supr U = ⊤), ∀ (i : ι), algebraic_geometry.is_open_immersion (f ∣_ U i)].tfae
theorem
algebraic_geometry.is_open_immersion.open_cover_iff
{X Y : algebraic_geometry.Scheme}
(𝒰 : Y.open_cover)
(f : X ⟶ Y) :