AlgebraicGeometry.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocallyNoetherian
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry
universe u
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocallyNoetherian in
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing inLean source · statement
theorem isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocallyNoetherian
{X M : Scheme.{u}} [IsLocallyNoetherian X] (ϖ : M ⟶ X) [LocallyOfFinitePresentation ϖ] [Mono ϖ]
(h : ∀ (T' T : Type u) [CommRing T'] [IsLocalRing T'] [IsArtinianRing T']
[CommRing T] [Nontrivial T] (p : T' →+* T), Function.Surjective p → RingHom.ker p *
maximalIdeal T' = ⊥ →
∀ (s : Spec (CommRingCat.of T') ⟶ X) (m : Spec (CommRingCat.of T) ⟶ M),
m ≫ ϖ = Spec.map (CommRingCat.ofHom p) ≫ s →
∃ m' : Spec (CommRingCat.of T') ⟶ M, m' ≫ ϖ = s ∧ Spec.map (CommRingCat.ofHom p) ≫ m' = m) :
IsOpenImmersion ϖ