Module

ArithmeticComponentResidue.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.Boundary.ArithmeticComponentResidue

2 declarations indexed from sourceView source ↗

Module documentation

Residue fields of arithmetic boundary components

The geometrically integral generic fibre supplied by the arithmetic boundary condition determines a geometrically integral residue field at the canonical generic point of every pulled-back boundary component.

Imports2

Imported by3

theorem

galoisPullback_componentGenericPoint_exists_geometricallyIntegralResidueAlgebra

L32 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.galoisPullback_componentGenericPoint_exists_geometricallyIntegralResidueAlgebra

Documentation

The residue field at the canonical generic point of a boundary component after a Galois finite-etale pullback is geometrically integral over the generic residue field of the arithmetic base. The required algebra structure is the canonical one transported through the generic fibre.

Source context 5 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.EffectiveCartierDivisor
universe u
variable {X S : Scheme.{u}}

Lean source · full declaration

theorem
    galoisPullback_componentGenericPoint_exists_geometricallyIntegralResidueAlgebra
    [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X] [IsIntegral S]
    (D : EffectiveCartierDivisor X) (p : X ⟶ S)
    (hD : D.SatisfiesResidueCharacteristicTwoBoundaryCondition p)
    (Y : FiniteEtale X) (hY : CategoryTheory.PreGaloisCategory.IsGalois Y)
    (Z : Set (D.1.comap Y.hom).subscheme)
    (hZ : Z ∈ irreducibleComponents (D.1.comap Y.hom).subscheme) :
    let I : Y.left.IdealSheafData := D.1.comap Y.hom
    let x := I.componentGenericPoint Z hZ
    let k := S.residueField (genericPoint S)
    ∃ hAlg : Algebra k (Y.left.residueField x),
      letI : Algebra k (Y.left.residueField x) := hAlg
      GeometricallyIntegral
        (Spec.map (CommRingCat.ofHom
          (algebraMap k (Y.left.residueField x)))) := by
  let : CategoryTheory.PreGaloisCategory.IsGalois Y := hY
  let : IsIntegral Y.left :=
    EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale Y
  let I : Y.left.IdealSheafData := D.1.comap Y.hom
  let C := I.subscheme.reducedIrreducibleComponent Z hZ
  let x := I.componentGenericPoint Z hZ
  let f : C ⟶ S := I.componentToBase (Y.hom ≫ p) Z hZ
  let i : C ⟶ Y.left :=
    I.subscheme.reducedIrreducibleComponentι Z hZ ≫ I.subschemeι
  have hchart :=
    D.galoisPullback_componentGenericPoint_chart p hD Y hY Z hZ
  dsimp only at hchart
  rcases hchart with ⟨_hregular, _hheight, hη, hgeo, _hchart⟩
  change ∃ hAlg : Algebra (S.residueField (genericPoint S))
      (Y.left.residueField x),
    letI : Algebra (S.residueField (genericPoint S))
      (Y.left.residueField x) := hAlg
    GeometricallyIntegral
      (Spec.map (CommRingCat.ofHom
        (algebraMap (S.residueField (genericPoint S))
          (Y.left.residueField x))))
  have hex :=
    i.exists_algebra_geometricallyIntegral_genericSourceResidue_of_genericFiber
      f hη hgeo
  have hix : i (genericPoint C) = x := by
    rfl
  rw [← hix]
  exact hex

theorem

galoisPullback_componentGenericPoint_localResidueData

L81 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.galoisPullback_componentGenericPoint_localResidueData