NYLL
Module

isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.lean

Nyll.AlgebraicCurves.Geometry.Schemes.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
30 declarations indexed from sourceView source ↗

Module documentation

is Open Immersion of mono of forall exists lift of is Artinian Ring of is Local Ring

Imports19
  • Mathlib.AlgebraicGeometry.Stalk
  • Mathlib.AlgebraicGeometry.ResidueField
  • Mathlib.AlgebraicGeometry.Morphisms.FlatMono
  • Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
  • Mathlib.AlgebraicGeometry.Morphisms.FiniteType
  • Mathlib.AlgebraicGeometry.Noetherian
  • Mathlib.Algebra.Category.Ring.Epi
  • Mathlib.Algebra.Algebra.Epi
  • Mathlib.RingTheory.HopkinsLevitzki
  • Mathlib.RingTheory.Filtration
  • Mathlib.RingTheory.Localization.Submodule
  • Mathlib.RingTheory.LocalRing.ResidueField.Basic
  • Mathlib.RingTheory.LocalRing.Quotient
  • Mathlib.RingTheory.TensorProduct.Finite
  • Mathlib.RingTheory.TensorProduct.Maps
  • Mathlib.LinearAlgebra.TensorProduct.Tower
  • Mathlib.Tactic.Abel
  • Mathlib.Tactic.Ring
  • Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Module_flat_of_maximalIdeal_rTensor_injective_of_isLocalHom
Imported by2

Declarations

theorem

epi_stalkMap_of_mono

L48 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bGlue.epi_stalkMap_of_mono
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
namespace E3bGlue
Lean source · statement
theorem epi_stalkMap_of_mono {M S : Scheme.{u}} (ϖ : M ⟶ S) [Mono ϖ] (x : M) : Epi (ϖ.stalkMap x)
theorem

exists_stalkHom_of_apply_closedPoint_eq

L58 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bGlue.exists_stalkHom_of_apply_closedPoint_eq
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
namespace E3bGlue
Lean source · statement
theorem exists_stalkHom_of_apply_closedPoint_eq {M : Scheme.{u}} {T : CommRingCat.{u}} [IsLocalRing
  T]
    (g : Spec T ⟶ M) (x : M) (hx : g.base (closedPoint T) = x) :
    ∃ ψ : M.presheaf.stalk x ⟶ T, IsLocalHom ψ.hom ∧ Spec.map ψ ≫ M.fromSpecStalk x = g
theorem

specMap_comp_fromSpecStalk_closedPoint

L65 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bGlue.specMap_comp_fromSpecStalk_closedPoint
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
namespace E3bGlue
Lean source · statement
theorem specMap_comp_fromSpecStalk_closedPoint {M : Scheme.{u}} {T : CommRingCat.{u}} [IsLocalRing
  T] {x : M}
    (ψ : M.presheaf.stalk x ⟶ T) [IsLocalHom ψ.hom] :
    (Spec.map ψ ≫ M.fromSpecStalk x).base (closedPoint T) = x
theorem

maximalIdeal_pow_ne_top

L79 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bGlue.maximalIdeal_pow_ne_top
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
namespace E3bGlue
section Quotients
variable (A : Type u) [CommRing A] [IsLocalRing A]
Lean source · statement
theorem maximalIdeal_pow_ne_top (n : ℕ) : maximalIdeal A ^ (n + 1) ≠ ⊤
instance

nontrivial_quot

L83 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bGlue.nontrivial_quot
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
namespace E3bGlue
section Quotients
variable (A : Type u) [CommRing A] [IsLocalRing A]
Lean source · statement
instance nontrivial_quot (n : ℕ) : Nontrivial (A ⧸ maximalIdeal A ^ (n + 1))
instance

isLocalRing_quot

L86 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bGlue.isLocalRing_quot
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
namespace E3bGlue
section Quotients
variable (A : Type u) [CommRing A] [IsLocalRing A]
Lean source · statement
instance isLocalRing_quot (n : ℕ) : IsLocalRing (A ⧸ maximalIdeal A ^ (n + 1))
theorem

eq_maximalIdeal_of_pow_le

L89 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bGlue.eq_maximalIdeal_of_pow_le
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
namespace E3bGlue
section Quotients
variable (A : Type u) [CommRing A] [IsLocalRing A]
Lean source · statement
theorem eq_maximalIdeal_of_pow_le {n : ℕ} (hn : n ≠ 0) (P : Ideal A) [P.IsPrime] (h : maximalIdeal
  A ^ n ≤ P) :
    P = maximalIdeal A
theorem

isMaximal_map_maximalIdeal

L95 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bGlue.isMaximal_map_maximalIdeal
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
namespace E3bGlue
section Quotients
variable (A : Type u) [CommRing A] [IsLocalRing A]
Lean source · statement
theorem isMaximal_map_maximalIdeal (n : ℕ) :
    ((maximalIdeal A).map (Ideal.Quotient.mk (maximalIdeal A ^ (n + 1)))).IsMaximal
theorem

isMaximal_of_isPrime_quot

L105 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bGlue.isMaximal_of_isPrime_quot
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
namespace E3bGlue
section Quotients
variable (A : Type u) [CommRing A] [IsLocalRing A]
Lean source · statement
theorem isMaximal_of_isPrime_quot (n : ℕ) (P : Ideal (A ⧸ maximalIdeal A ^ (n + 1))) (hP :
  P.IsPrime) : P.IsMaximal
instance

isArtinianRing_quot

L119 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bGlue.isArtinianRing_quot
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
namespace E3bGlue
section Quotients
variable (A : Type u) [CommRing A] [IsLocalRing A]
Lean source · statement
instance isArtinianRing_quot [IsNoetherianRing A] (n : ℕ) : IsArtinianRing (A ⧸ maximalIdeal
  A ^ (n + 1))
theorem

maximalIdeal_quot

L124 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bGlue.maximalIdeal_quot
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
namespace E3bGlue
section Quotients
variable (A : Type u) [CommRing A] [IsLocalRing A]
Lean source · statement
theorem maximalIdeal_quot (n : ℕ) :
    maximalIdeal (A ⧸ maximalIdeal A ^ (n + 1)) = (maximalIdeal A).map (Ideal.Quotient.mk
      (maximalIdeal A ^ (n + 1)))
theorem

factor_surjective

L129 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bGlue.factor_surjective
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
namespace E3bGlue
section Quotients
variable (A : Type u) [CommRing A] [IsLocalRing A]
Lean source · statement
theorem factor_surjective (n : ℕ) :
    Function.Surjective (Ideal.Quotient.factor
      (Ideal.pow_le_pow_right (Nat.le_succ (n + 1)) : maximalIdeal A ^ (n + 1 + 1) ≤ maximalIdeal A
        ^ (n + 1)))
theorem

ker_factor

L137 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bGlue.ker_factor
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
namespace E3bGlue
section Quotients
variable (A : Type u) [CommRing A] [IsLocalRing A]
Lean source · statement
theorem ker_factor (n : ℕ) :
    RingHom.ker (Ideal.Quotient.factor
        (Ideal.pow_le_pow_right (Nat.le_succ (n + 1)) : maximalIdeal A ^ (n + 1 + 1) ≤ maximalIdeal
          A ^ (n + 1))) =
      (maximalIdeal A ^ (n + 1)).map (Ideal.Quotient.mk (maximalIdeal A ^ (n + 1 + 1)))
theorem

ker_factor_mul_maximalIdeal

L154 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bGlue.ker_factor_mul_maximalIdeal
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
namespace E3bGlue
section Quotients
variable (A : Type u) [CommRing A] [IsLocalRing A]
Lean source · statement
theorem ker_factor_mul_maximalIdeal (n : ℕ) :
    RingHom.ker (Ideal.Quotient.factor
        (Ideal.pow_le_pow_right (Nat.le_succ (n + 1)) : maximalIdeal A ^ (n + 1 + 1) ≤ maximalIdeal
          A ^ (n + 1))) *
      maximalIdeal (A ⧸ maximalIdeal A ^ (n + 1 + 1)) = ⊥
theorem

exists_retraction_succ

L172 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bGlue.exists_retraction_succ
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
namespace E3bGlue
Lean source · statement
theorem exists_retraction_succ {R : Type u} [CommRing R] {M : Scheme.{u}} (ϖ : M ⟶ Spec
  (CommRingCat.of R)) [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') ⟶ Spec (CommRingCat.of R)) (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)
    (x : M) (n : ℕ) [IsNoetherianRing ((Spec (CommRingCat.of R)).presheaf.stalk (ϖ.base x))]
    (ψ : M.presheaf.stalk x ⟶ CommRingCat.of (↑((Spec (CommRingCat.of R)).presheaf.stalk (ϖ.base
      x)) ⧸ maximalIdeal ↑((Spec (CommRingCat.of R)).presheaf.stalk (ϖ.base x)) ^ (n + 1)))
      [IsLocalHom ψ.hom]
    (hψ : ϖ.stalkMap x ≫ ψ = CommRingCat.ofHom (Ideal.Quotient.mk (maximalIdeal ↑((Spec
      (CommRingCat.of R)).presheaf.stalk (ϖ.base x)) ^ (n + 1)))) :
    ∃ ψ' : M.presheaf.stalk x ⟶ CommRingCat.of (↑((Spec (CommRingCat.of R)).presheaf.stalk (ϖ.base
      x)) ⧸ maximalIdeal ↑((Spec (CommRingCat.of R)).presheaf.stalk (ϖ.base x)) ^ (n + 1 + 1)),
      IsLocalHom ψ'.hom ∧ ϖ.stalkMap x ≫ ψ' = CommRingCat.ofHom (Ideal.Quotient.mk (maximalIdeal
        ↑((Spec (CommRingCat.of R)).presheaf.stalk (ϖ.base x)) ^ (n + 1 + 1)))
theorem

isNoetherianRing_stalk

L243 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bGlue.isNoetherianRing_stalk
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
namespace E3bGlue
Lean source · statement
theorem isNoetherianRing_stalk {R : Type u} [CommRing R] [IsNoetherianRing R] (p : ↥(Spec
  (CommRingCat.of R))) :
    IsNoetherianRing ((Spec (CommRingCat.of R)).presheaf.stalk p)
theorem

maximalIdeal_pow_smul_top_le_restrictScalars

L267 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bMono.maximalIdeal_pow_smul_top_le_restrictScalars
Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
namespace E3bMono
section separated
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] [IsLocalRing A] [IsLocalRing B]
  [IsLocalHom (algebraMap A B)]
Lean source · statement
theorem maximalIdeal_pow_smul_top_le_restrictScalars (P : Type*) [AddCommGroup P] [Module A P]
    [Module B P] [IsScalarTower A B P] (k : ℕ) :
    ((maximalIdeal A) ^ k • ⊤ : Submodule A P) ≤
      ((maximalIdeal B) ^ k • ⊤ : Submodule B P).restrictScalars A
theorem

iInf_maximalIdeal_pow_smul_eq_bot_of_isLocalHom

L283 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bMono.iInf_maximalIdeal_pow_smul_eq_bot_of_isLocalHom
Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
namespace E3bMono
section separated
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] [IsLocalRing A] [IsLocalRing B]
  [IsLocalHom (algebraMap A B)]
variable [IsNoetherianRing B]
Lean source · statement
theorem iInf_maximalIdeal_pow_smul_eq_bot_of_isLocalHom (P : Type*) [AddCommGroup P]
    [Module A P] [Module B P] [IsScalarTower A B P] [Module.Finite B P] :
    (⨅ k : ℕ, (maximalIdeal A) ^ k • ⊤ : Submodule A P) = ⊥
theorem

finite_lTensor

L314 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bMono.finite_lTensor
Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
namespace E3bMono
attribute [local instance]
  E3bGlue.nontrivial_quot
attribute [local instance]
  E3bGlue.isLocalRing_quot
attribute [local instance]
  E3bGlue.isArtinianRing_quot
Lean source · statement
theorem finite_lTensor {A : Type u} (B : Type u) [CommRing A] [CommRing B] [Algebra A B]
    (M : Type u) [AddCommGroup M] [Module A M] [Module B M] [IsScalarTower A B M]
    [Module.Finite B M] (P : Type u) [AddCommGroup P] [Module A P] [Module.Finite A P] :
    Module.Finite B (M ⊗[A] P)
theorem

iInf_maximalIdeal_pow_smul_tensor_eq_bot

L320 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bMono.iInf_maximalIdeal_pow_smul_tensor_eq_bot
Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
namespace E3bMono
attribute [local instance]
  E3bGlue.nontrivial_quot
attribute [local instance]
  E3bGlue.isLocalRing_quot
attribute [local instance]
  E3bGlue.isArtinianRing_quot
Lean source · statement
theorem iInf_maximalIdeal_pow_smul_tensor_eq_bot {A : Type u} (B : Type u)
    [CommRing A] [CommRing B] [Algebra A B] [IsLocalRing A] [IsLocalRing B]
    [IsLocalHom (algebraMap A B)] [IsNoetherianRing B]
    (M : Type u) [AddCommGroup M] [Module A M] [Module B M] [IsScalarTower A B M]
    [Module.Finite B M] (P : Type u) [AddCommGroup P] [Module A P] [Module.Finite A P] :
    (⨅ k : ℕ, (maximalIdeal A) ^ k • ⊤ : Submodule A (M ⊗[A] P)) = ⊥
lemma

map_mem_smul_top

L333 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bMono.map_mem_smul_top
Source context 20 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
namespace E3bMono
attribute [local instance]
  E3bGlue.nontrivial_quot
attribute [local instance]
  E3bGlue.isLocalRing_quot
attribute [local instance]
  E3bGlue.isArtinianRing_quot
section core
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
lemma map_mem_smul_top {P Q : Type*} [AddCommGroup P] [Module A P] [AddCommGroup Q] [Module A Q]
    (g : P →ₗ[A] Q) {I : Ideal A} {p : P} (hp : p ∈ (I • ⊤ : Submodule A P)) :
    g p ∈ (I • ⊤ : Submodule A Q)
lemma

mem_pow_smul_top_of_coe_mem

L340 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bMono.mem_pow_smul_top_of_coe_mem
Source context 20 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
namespace E3bMono
attribute [local instance]
  E3bGlue.nontrivial_quot
attribute [local instance]
  E3bGlue.isLocalRing_quot
attribute [local instance]
  E3bGlue.isArtinianRing_quot
section core
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
lemma mem_pow_smul_top_of_coe_mem (I : Ideal A) (k : ℕ) (m : I) (hm : (m : A) ∈ I ^ k * I) :
    m ∈ (I ^ k • ⊤ : Submodule A I)
theorem

lTensor_maximalIdeal_subtype_injective

L352 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bMono.lTensor_maximalIdeal_subtype_injective
Source context 21 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
namespace E3bMono
attribute [local instance]
  E3bGlue.nontrivial_quot
attribute [local instance]
  E3bGlue.isLocalRing_quot
attribute [local instance]
  E3bGlue.isArtinianRing_quot
section core
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
variable [IsNoetherianRing A] [IsNoetherianRing B] [IsLocalRing A] [IsLocalRing B]
  [IsLocalHom (algebraMap A B)]
Lean source · statement
theorem lTensor_maximalIdeal_subtype_injective
    (hI : ∀ k : ℕ, ∀ b : B, ∃ a : A,
      b - algebraMap A B a ∈ (maximalIdeal A ^ k • ⊤ : Submodule A B))
    (hII : ∀ k : ℕ, ∀ a : A,
      algebraMap A B a ∈ (maximalIdeal A ^ k • ⊤ : Submodule A B) → a ∈ maximalIdeal A ^ k) :
    Function.Injective (LinearMap.lTensor B (maximalIdeal A).subtype)
theorem

flat_of_approx

L407 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bMono.flat_of_approx
Source context 21 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
namespace E3bMono
attribute [local instance]
  E3bGlue.nontrivial_quot
attribute [local instance]
  E3bGlue.isLocalRing_quot
attribute [local instance]
  E3bGlue.isArtinianRing_quot
section core
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
variable [IsNoetherianRing A] [IsNoetherianRing B] [IsLocalRing A] [IsLocalRing B]
  [IsLocalHom (algebraMap A B)]
Lean source · statement
theorem flat_of_approx
    (hI : ∀ k : ℕ, ∀ b : B, ∃ a : A,
      b - algebraMap A B a ∈ (maximalIdeal A ^ k • ⊤ : Submodule A B))
    (hII : ∀ k : ℕ, ∀ a : A,
      algebraMap A B a ∈ (maximalIdeal A ^ k • ⊤ : Submodule A B) → a ∈ maximalIdeal A ^ k) :
    Module.Flat A B
theorem

approx_of_isEpi_of_retraction

L436 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bMono.approx_of_isEpi_of_retraction
Source context 23 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
namespace E3bMono
attribute [local instance]
  E3bGlue.nontrivial_quot
attribute [local instance]
  E3bGlue.isLocalRing_quot
attribute [local instance]
  E3bGlue.isArtinianRing_quot
attribute [local instance]
  E3bGlue.nontrivial_quot
attribute [local instance]
  E3bGlue.isLocalRing_quot
attribute [local instance]
  E3bGlue.isArtinianRing_quot
section retraction
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
theorem approx_of_isEpi_of_retraction [Algebra.IsEpi A B] (I : Ideal A)
    (ψ : B →+* A ⧸ I) (hψ : ψ.comp (algebraMap A B) = Ideal.Quotient.mk I) :
    (∀ b : B, ∃ a : A, b - algebraMap A B a ∈ (I • ⊤ : Submodule A B)) ∧
    (∀ a : A, algebraMap A B a ∈ (I • ⊤ : Submodule A B) → a ∈ I)
theorem

surjective_algebraMap_of_isEpi_of_field

L499 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bMono.surjective_algebraMap_of_isEpi_of_field
Source context 25 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
namespace E3bMono
attribute [local instance]
  E3bGlue.nontrivial_quot
attribute [local instance]
  E3bGlue.isLocalRing_quot
attribute [local instance]
  E3bGlue.isArtinianRing_quot
attribute [local instance]
  E3bGlue.nontrivial_quot
attribute [local instance]
  E3bGlue.isLocalRing_quot
attribute [local instance]
  E3bGlue.isArtinianRing_quot
attribute [local instance]
  E3bGlue.nontrivial_quot
attribute [local instance]
  E3bGlue.isLocalRing_quot
attribute [local instance]
  E3bGlue.isArtinianRing_quot
section fieldEpi
Lean source · statement
theorem surjective_algebraMap_of_isEpi_of_field (K L : Type u) [Field K] [Field L] [Algebra K L]
    [Algebra.IsEpi K L] : Function.Surjective (algebraMap K L)
theorem

residueField_algebraMap_bijective_of_isEpi

L529 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bMono.residueField_algebraMap_bijective_of_isEpi
Source context 26 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
namespace E3bMono
attribute [local instance]
  E3bGlue.nontrivial_quot
attribute [local instance]
  E3bGlue.isLocalRing_quot
attribute [local instance]
  E3bGlue.isArtinianRing_quot
attribute [local instance]
  E3bGlue.nontrivial_quot
attribute [local instance]
  E3bGlue.isLocalRing_quot
attribute [local instance]
  E3bGlue.isArtinianRing_quot
attribute [local instance]
  E3bGlue.nontrivial_quot
attribute [local instance]
  E3bGlue.isLocalRing_quot
attribute [local instance]
  E3bGlue.isArtinianRing_quot
section fieldEpi
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] [IsLocalRing A] [IsLocalRing B]
  [IsLocalHom (algebraMap A B)]
Lean source · statement
theorem residueField_algebraMap_bijective_of_isEpi [Algebra.IsEpi A B] :
    Function.Bijective (algebraMap (ResidueField A) (ResidueField B))
theorem

exists_retraction_one

L549 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bMono.exists_retraction_one
Source context 26 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
namespace E3bMono
attribute [local instance]
  E3bGlue.nontrivial_quot
attribute [local instance]
  E3bGlue.isLocalRing_quot
attribute [local instance]
  E3bGlue.isArtinianRing_quot
attribute [local instance]
  E3bGlue.nontrivial_quot
attribute [local instance]
  E3bGlue.isLocalRing_quot
attribute [local instance]
  E3bGlue.isArtinianRing_quot
attribute [local instance]
  E3bGlue.nontrivial_quot
attribute [local instance]
  E3bGlue.isLocalRing_quot
attribute [local instance]
  E3bGlue.isArtinianRing_quot
section fieldEpi
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] [IsLocalRing A] [IsLocalRing B]
  [IsLocalHom (algebraMap A B)]
Lean source · statement
theorem exists_retraction_one [Algebra.IsEpi A B] :
    ∃ ψ : B →+* A ⧸ maximalIdeal A ^ 1,
      IsLocalHom ψ ∧ ψ.comp (algebraMap A B) = Ideal.Quotient.mk _
theorem

flat_stalkMap

L595 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing.E3bMono.flat_stalkMap
Source context 28 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing TensorProduct
universe u
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
namespace E3bMono
attribute [local instance]
  E3bGlue.nontrivial_quot
attribute [local instance]
  E3bGlue.isLocalRing_quot
attribute [local instance]
  E3bGlue.isArtinianRing_quot
attribute [local instance]
  E3bGlue.nontrivial_quot
attribute [local instance]
  E3bGlue.isLocalRing_quot
attribute [local instance]
  E3bGlue.isArtinianRing_quot
attribute [local instance]
  E3bGlue.nontrivial_quot
attribute [local instance]
  E3bGlue.isLocalRing_quot
attribute [local instance]
  E3bGlue.isArtinianRing_quot
attribute [local instance]
  E3bGlue.nontrivial_quot
attribute [local instance]
  E3bGlue.isLocalRing_quot
attribute [local instance]
  E3bGlue.isArtinianRing_quot
section assembly
Lean source · statement
theorem flat_stalkMap {R : Type u} [CommRing R] [IsNoetherianRing R] {M : Scheme.{u}}
    (ϖ : M ⟶ Spec (CommRingCat.of R)) [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') ⟶ Spec (CommRingCat.of R)) (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)
    (x : M) : (ϖ.stalkMap x).hom.Flat
theorem

isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing

L685 ↗
AlgebraicGeometry.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits IsLocalRing TensorProduct
universe u
attribute [local instance] E3bGlue.nontrivial_quot
attribute [local instance] E3bGlue.isLocalRing_quot
attribute [local instance] E3bGlue.isArtinianRing_quot
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing in
open E3bMono in
Lean source · statement
theorem isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
    {R : Type u} [CommRing R] [IsNoetherianRing R] {M : Scheme.{u}} (ϖ : M ⟶ Spec (CommRingCat.of
      R))
    [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') ⟶ Spec (CommRingCat.of R)) (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 ϖ

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.