Module

FiniteNeighborhoodSection.lean

Nyll.SchemeTheory.Etale.FiniteNeighborhoodSection

3 declarations indexed from sourceView source ↗

Module documentation

Sections over neighborhoods of a finite base

A neighborhood containing a fiber of a closed morphism contains the inverse image of a neighborhood on the base. Applied to the isomorphism neighborhood of a finite étale morphism, this constructs a section over a neighborhood on the base of a finite universally injective morphism.

Imports9

Nyll.SchemeTheory.Etale.IsomorphismNeighborhood
Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Mathlib.AlgebraicGeometry.Restrict
Mathlib.RingTheory.Etale.QuasiFinite
Mathlib.RingTheory.Finiteness.Basic
Mathlib.RingTheory.Spectrum.Prime.Topology

Imported by5

theorem

exists_etale_finite_factor_of_quasiFiniteAt

L41 ↗

AlgebraicGeometry.exists_etale_finite_factor_of_quasiFiniteAt

Documentation

The idempotent supplied by the étale local structure theorem gives an actual finite open factor with a singleton fiber. The point of this factor maps to the prescribed prime of the original algebra, and the residue field of the chosen point on the étale base is unchanged.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits TopologicalSpace
open scoped TensorProduct
universe u
namespace AlgebraicGeometry

Lean source · statement

theorem exists_etale_finite_factor_of_quasiFiniteAt
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.FiniteType R S] (p : Ideal R) [p.IsPrime]
    (q : Ideal S) [q.IsPrime] [q.LiesOver p] [Algebra.QuasiFiniteAt R q] :
    ∃ (R' : Type u) (_ : CommRing R') (_ : Algebra R R') (_ : Algebra.Etale R R')
      (P : Ideal R') (_ : P.IsPrime) (_ : P.LiesOver p)
      (e : R' ⊗[R] S) (_ : IsIdempotentElem e),
      Function.Bijective (Ideal.ResidueField.mapₐ p P (Algebra.ofId _ _) (P.over_def p)) ∧
      Module.Finite R' (Localization.Away e) ∧
      IsFinite (Spec.map (CommRingCat.ofHom (algebraMap R' (Localization.Away e)))) ∧
      IsOpenImmersion (Spec.map (CommRingCat.ofHom
        (algebraMap (R' ⊗[R] S) (Localization.Away e)))) ∧
      ∃ z : Spec (CommRingCat.of (Localization.Away e)),
        Spec.map (CommRingCat.ofHom (algebraMap R' (Localization.Away e))) z =
          ⟨P, inferInstance⟩ ∧
        (Spec.map (CommRingCat.ofHom (algebraMap (R' ⊗[R] S) (Localization.Away e))) ≫
          Spec.map (CommRingCat.ofHom
            (Algebra.TensorProduct.includeRight : S →ₐ[R] R' ⊗[R] S).toRingHom)) z =
          (⟨q, inferInstance⟩ : Spec (CommRingCat.of S)) ∧
        ∀ z' : Spec (CommRingCat.of (Localization.Away e)),
          Spec.map (CommRingCat.ofHom (algebraMap R' (Localization.Away e))) z' =
            ⟨P, inferInstance⟩ → z' = z

theorem

exists_preimage_le_of_fiber_subset

L115 ↗

AlgebraicGeometry.Scheme.Hom.exists_preimage_le_of_fiber_subset

Documentation

A neighborhood containing a whole fiber of a universally closed morphism contains the inverse image of an open neighborhood of the base point.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits TopologicalSpace
open scoped TensorProduct
universe u
namespace AlgebraicGeometry

Lean source · statement

theorem Scheme.Hom.exists_preimage_le_of_fiber_subset
    {X Y : Scheme.{u}} (f : X ⟶ Y) [UniversallyClosed f]
    (y : Y) (U : X.Opens) (hU : ∀ x : X, f x = y → x ∈ U) :
    ∃ V : Y.Opens, y ∈ V ∧ f ⁻¹ᵁ V ≤ U

theorem

exists_section_over_finite_base_neighborhood

L131 ↗

AlgebraicGeometry.Etale.exists_section_over_finite_base_neighborhood

Documentation

A finite étale morphism with a singleton fiber and purely inseparable residue extension has a section over the inverse image of a neighborhood on a finite universally injective base. The section passes through the specified point.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits TopologicalSpace
open scoped TensorProduct
universe u
namespace AlgebraicGeometry

Lean source · statement

theorem Etale.exists_section_over_finite_base_neighborhood
    {U X Y : Scheme.{u}} (p : U ⟶ X) (f : X ⟶ Y)
    [IsFinite p] [Etale p] [IsFinite f] [UniversallyInjective f]
    (u : U) (hu : ∀ u' : U, p u' = p u → u' = u)
    (hκ : (p.residueFieldMap u).hom.IsPurelyInseparable) :
    ∃ (V : Y.Opens) (hV : f (p u) ∈ V)
      (s : (f ⁻¹ᵁ V).toScheme ⟶ U),
      s ≫ p = (f ⁻¹ᵁ V).ι ∧ s ⟨p u, hV⟩ = u

Module documentation

Sections over neighborhoods of a finite base

Declarations

exists_etale_finite_factor_of_quasiFiniteAt

exists_preimage_le_of_fiber_subset

exists_section_over_finite_base_neighborhood