NYLL
Module

GeometricStalkGenericColimit.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkGenericColimit
10 declarations indexed from sourceView source ↗

Module documentation

The actual strict generic field as a filtered colimit

Base-change the already constructed small pointed-neighborhood diagram from R to its actual fraction field K. Its colimit is K ⊗[R] A, where A is the actual geometric stalk. The existing fraction-tensor comparison identifies this ring with Frac(A). Its K-scalar map is the existing geometricStalkFractionFieldMap: fraction-ring extensionality reduces the comparison to the original map R → A.

Transporting the actual base-changed cocone along this K-algebra equivalence gives a filtered colimit with vertex the actual strict generic field. The literal cocone-leg formula retains both the fraction-field map and the actual geometric-stalk germ maps.

This constructs the colimit required for finite-presentation descent over K, without requiring finite presentation of K over R. It is a prerequisite for Stacks, Tag 0BSM, not the full exact-sequence result.

Imports13
Imported by2

Declarations

def

geometricStalkGenericFieldEquiv

L55 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkGenericFieldEquiv
Documentation

The generic tensor comparison respects the actual original fraction-field map, rather than an independently chosen action on the strict generic field.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
  [IsLocalRing R] [Field Ω] (φ : R →+* Ω) [IsLocalHom φ]
Lean source · full declaration
def geometricStalkGenericFieldEquiv :
    letI : Algebra R (geometricStalk (Spec.map (CommRingCat.ofHom φ))) :=
      (geometricStalkStructureMap φ).toAlgebra
    letI : Algebra (FractionRing R)
        (FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom φ)))) :=
      (geometricStalkFractionFieldMap φ).toAlgebra
    (FractionRing R ⊗[R] geometricStalk (Spec.map (CommRingCat.ofHom φ))) ≃ₐ[FractionRing R]
      FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom φ))) := by
  let A := geometricStalk (Spec.map (CommRingCat.ofHom φ))
  let K := FractionRing R
  let F := FractionRing A
  letI : Algebra R A := (geometricStalkStructureMap φ).toAlgebra
  letI : Algebra K F := (geometricStalkFractionFieldMap φ).toAlgebra
  let e : (A ⊗[R] K) ≃ₐ[A] F := geometricStalkFractionTensorEquiv φ
  have hmap : e.toRingHom.comp
      (Algebra.TensorProduct.includeRight : K →ₐ[R] (A ⊗[R] K)).toRingHom =
      geometricStalkFractionFieldMap φ := by
    apply IsFractionRing.ringHom_ext (A := R)
    intro r
    change e ((Algebra.TensorProduct.includeRight : K →ₐ[R] (A ⊗[R] K))
      (algebraMap R K r)) = geometricStalkFractionFieldMap φ (algebraMap R K r)
    rw [AlgHom.commutes]
    change e (algebraMap A (A ⊗[R] K) (geometricStalkStructureMap φ r)) = _
    rw [e.commutes]
    exact (geometricStalkFractionFieldMap_algebraMap φ r).symm
  refine
    { __ := (Algebra.TensorProduct.comm R K A).toRingEquiv.trans e.toRingEquiv
      commutes' := ?_ }
  intro k
  change e ((Algebra.TensorProduct.comm R K A) (k ⊗ₜ[R] (1 : A))) =
    geometricStalkFractionFieldMap φ k
  rw [Algebra.TensorProduct.comm_tmul]
  exact RingHom.congr_fun hmap k
theorem

geometricStalkGenericFieldEquiv_one_tmul

L91 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkGenericFieldEquiv_one_tmul
Documentation

On stalk elements the generic comparison is the canonical inclusion in the actual fraction field.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
  [IsLocalRing R] [Field Ω] (φ : R →+* Ω) [IsLocalHom φ]
Lean source · full declaration
theorem geometricStalkGenericFieldEquiv_one_tmul
    (a : geometricStalk (Spec.map (CommRingCat.ofHom φ))) :
    let : Algebra R (geometricStalk (Spec.map (CommRingCat.ofHom φ))) :=
      (geometricStalkStructureMap φ).toAlgebra
    let : Algebra (FractionRing R)
        (FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom φ)))) :=
      (geometricStalkFractionFieldMap φ).toAlgebra
    geometricStalkGenericFieldEquiv φ ((1 : FractionRing R) ⊗ₜ[R] a) =
      algebraMap (geometricStalk (Spec.map (CommRingCat.ofHom φ)))
        (FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom φ)))) a := by
  let A := geometricStalk (Spec.map (CommRingCat.ofHom φ))
  let : Algebra R A := (geometricStalkStructureMap φ).toAlgebra
  let : Algebra (FractionRing R) (FractionRing A) :=
    (geometricStalkFractionFieldMap φ).toAlgebra
  change geometricStalkFractionTensorEquiv φ
    (algebraMap A (A ⊗[R] FractionRing R) a) = algebraMap A (FractionRing A) a
  exact (geometricStalkFractionTensorEquiv φ).commutes a
theorem

geometricStalkGenericFieldEquiv_tmul

L110 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkGenericFieldEquiv_tmul
Documentation

The generic comparison retains both literal factor maps.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
  [IsLocalRing R] [Field Ω] (φ : R →+* Ω) [IsLocalHom φ]
Lean source · full declaration
theorem geometricStalkGenericFieldEquiv_tmul (k : FractionRing R)
    (a : geometricStalk (Spec.map (CommRingCat.ofHom φ))) :
    let : Algebra R (geometricStalk (Spec.map (CommRingCat.ofHom φ))) :=
      (geometricStalkStructureMap φ).toAlgebra
    let : Algebra (FractionRing R)
        (FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom φ)))) :=
      (geometricStalkFractionFieldMap φ).toAlgebra
    geometricStalkGenericFieldEquiv φ (k ⊗ₜ[R] a) =
      geometricStalkFractionFieldMap φ k *
        algebraMap (geometricStalk (Spec.map (CommRingCat.ofHom φ)))
          (FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom φ)))) a := by
  let A := geometricStalk (Spec.map (CommRingCat.ofHom φ))
  let K := FractionRing R
  let : Algebra R A := (geometricStalkStructureMap φ).toAlgebra
  let : Algebra K (FractionRing A) := (geometricStalkFractionFieldMap φ).toAlgebra
  let e : (K ⊗[R] A) ≃ₐ[K] FractionRing A := geometricStalkGenericFieldEquiv φ
  calc
    e (k ⊗ₜ[R] a) = e ((k ⊗ₜ[R] (1 : A)) * ((1 : K) ⊗ₜ[R] a)) := by
      rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]
    _ = e (k ⊗ₜ[R] (1 : A)) * e ((1 : K) ⊗ₜ[R] a) := map_mul e _ _
    _ = geometricStalkFractionFieldMap φ k * algebraMap A (FractionRing A) a := by
      change e (algebraMap K (K ⊗[R] A) k) * e ((1 : K) ⊗ₜ[R] a) = _
      rw [e.commutes]
      exact congrArg (fun z => geometricStalkFractionFieldMap φ k * z)
        (geometricStalkGenericFieldEquiv_one_tmul φ a)
def

geometricStalkSmallGenericAlgebraDiagram

L139 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkSmallGenericAlgebraDiagram
Documentation

Generic fibers of the actual small pointed étale-neighborhood diagram.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
  [IsLocalRing R] [Field Ω] (φ : R →+* Ω) [IsLocalHom φ]
variable [IsSepClosed Ω]
Lean source · statement
def geometricStalkSmallGenericAlgebraDiagram :
    GeometricStalkAlgebraIndex φ ⥤ Under (CommRingCat.of (FractionRing R))
def

geometricStalkGenericTensorCocone

L145 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkGenericTensorCocone
Documentation

Base change of the actual germ cocone, with its literal tensor vertex.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
  [IsLocalRing R] [Field Ω] (φ : R →+* Ω) [IsLocalHom φ]
variable [IsSepClosed Ω]
Lean source · statement
def geometricStalkGenericTensorCocone : Cocone (geometricStalkSmallGenericAlgebraDiagram φ)
def

geometricStalkGenericTensorCoconeIsColimit

L150 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkGenericTensorCoconeIsColimit
Documentation

Tensor base change preserves the already constructed small colimit.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
  [IsLocalRing R] [Field Ω] (φ : R →+* Ω) [IsLocalHom φ]
variable [IsSepClosed Ω]
Lean source · statement
def geometricStalkGenericTensorCoconeIsColimit :
    IsColimit (geometricStalkGenericTensorCocone φ)
def

geometricStalkGenericFieldVertexIso

L162 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkGenericFieldVertexIso
Documentation

The constructed comparison between the two actual vertices in Under K. Its endpoints name the existing tensor cocone and the existing fraction-field map explicitly, so later cocone transport reuses this single typed owner.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
  [IsLocalRing R] [Field Ω] (φ : R →+* Ω) [IsLocalHom φ]
variable [IsSepClosed Ω]
Lean source · statement
def geometricStalkGenericFieldVertexIso :
    (geometricStalkGenericTensorCocone φ).pt ≅
      Under.mk (CommRingCat.ofHom (geometricStalkFractionFieldMap φ))
def

geometricStalkGenericFieldCocone

L173 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkGenericFieldCocone
Documentation

The actual strict generic field is the vertex, with the actual induced fraction-field scalar map.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
  [IsLocalRing R] [Field Ω] (φ : R →+* Ω) [IsLocalHom φ]
variable [IsSepClosed Ω]
Lean source · statement
def geometricStalkGenericFieldCocone : Cocone (geometricStalkSmallGenericAlgebraDiagram φ)
def

geometricStalkGenericFieldCoconeIsColimit

L178 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkGenericFieldCoconeIsColimit
Documentation

The actual strict generic field cocone is colimiting; its vertex comparison is constructed, not included as an input.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
  [IsLocalRing R] [Field Ω] (φ : R →+* Ω) [IsLocalHom φ]
variable [IsSepClosed Ω]
Lean source · statement
def geometricStalkGenericFieldCoconeIsColimit :
    IsColimit (geometricStalkGenericFieldCocone φ)
theorem

geometricStalkGenericFieldCocone_tmul

L186 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkGenericFieldCocone_tmul
Documentation

The actual generic cocone leg is the fraction-field scalar times the fraction-field image of the original actual germ cocone leg.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
  [IsLocalRing R] [Field Ω] (φ : R →+* Ω) [IsLocalHom φ]
variable [IsSepClosed Ω]
Lean source · full declaration
theorem geometricStalkGenericFieldCocone_tmul (i : GeometricStalkAlgebraIndex φ)
    (k : FractionRing R) (z : (geometricStalkSmallAlgebraDiagram φ).obj i) :
    let : Algebra R ((geometricStalkSmallAlgebraDiagram φ).obj i).right :=
      ((geometricStalkSmallAlgebraDiagram φ).obj i).hom.hom.toAlgebra
    ((geometricStalkGenericFieldCocone φ).ι.app i).right (k ⊗ₜ[R] z) =
      geometricStalkFractionFieldMap φ k *
        algebraMap (geometricStalk (Spec.map (CommRingCat.ofHom φ)))
          (FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom φ))))
          (((geometricStalkSmallAlgebraCocone φ).ι.app i).right z) := by
  let : Algebra R ((geometricStalkSmallAlgebraDiagram φ).obj i).right :=
    ((geometricStalkSmallAlgebraDiagram φ).obj i).hom.hom.toAlgebra
  let A := geometricStalk (Spec.map (CommRingCat.ofHom φ))
  let : Algebra R A := (geometricStalkStructureMap φ).toAlgebra
  let : Algebra (FractionRing R) (FractionRing A) :=
    (geometricStalkFractionFieldMap φ).toAlgebra
  change geometricStalkGenericFieldEquiv φ
    (filteredBaseChangeCoconeLegAlgHom (A := FractionRing R)
      (geometricStalkSmallAlgebraCocone φ) i (k ⊗ₜ[R] z)) = _
  rw [filteredBaseChangeCoconeLegAlgHom_tmul]
  exact geometricStalkGenericFieldEquiv_tmul φ k
    (CommRingCat.toAlgHom ((geometricStalkSmallAlgebraCocone φ).ι.app i) z)

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