Module

ArithmeticDagger.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.Boundary.ArithmeticDagger

3 declarations indexed from sourceView source ↗

Module documentation

Arithmetic boundary stability under Galois covers

The full residue-characteristic-two boundary condition is inherited by a connected finite-etale Galois pullback. In particular, the result includes the geometric-integrality clause after every further connected Galois cover. Only local Noetherianity is used.

Imports3

Imported by1

Nyll.EtaleFundamentalGroups.FiniteEtale.Boundary.All

theorem

galoisPullback_satisfiesResidueCharacteristicTwoBoundaryCondition

L33 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.galoisPullback_satisfiesResidueCharacteristicTwoBoundaryCondition

Documentation

A connected finite-etale Galois pullback preserves the complete residue-characteristic-two arithmetic boundary condition.

Source context 6 commands

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

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

Lean source · full declaration

theorem galoisPullback_satisfiesResidueCharacteristicTwoBoundaryCondition
    [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) :
    letI : CategoryTheory.PreGaloisCategory.IsGalois Y := hY
    letI : IsIntegral Y.left :=
      isIntegral_left_of_isConnected_finiteEtale Y
    letI : IsNormalIntegral Y.left :=
      isNormalIntegral_left_of_isConnected_finiteEtale Y
    letI : IsLocallyNoetherian Y.left :=
      isLocallyNoetherian_left_finiteEtale Y
    let D' : EffectiveCartierDivisor Y.left := D.comapFiniteEtale Y
    D'.SatisfiesResidueCharacteristicTwoBoundaryCondition (Y.hom ≫ p) := by
  let : CategoryTheory.PreGaloisCategory.IsGalois Y := hY
  let : IsIntegral Y.left :=
    isIntegral_left_of_isConnected_finiteEtale Y
  let : IsNormalIntegral Y.left :=
    isNormalIntegral_left_of_isConnected_finiteEtale Y
  let : IsLocallyNoetherian Y.left :=
    isLocallyNoetherian_left_finiteEtale Y
  let D' : EffectiveCartierDivisor Y.left := D.comapFiniteEtale Y
  have hstable := D.galoisPullback_stability p hD Y hY
  dsimp only at hstable
  rcases hstable with ⟨hreduced, hhorizontal, hregular, hcomponents⟩
  refine ⟨hreduced, hhorizontal, hregular, ?_, ?_⟩
  · intro Z hZ
    exact (hcomponents Z hZ).2
  · intro Zc hZc F hF
    let : CategoryTheory.PreGaloisCategory.IsGalois Zc := hZc
    change GeometricallyIntegral
      ((((D.1.comap Y.hom).comap Zc.hom).componentToBase
        (Zc.hom ≫ (Y.hom ≫ p)) F hF).fiberToSpecResidueField
          (genericPoint S))
    rw [← Category.assoc]
    exact D.geometricallyIntegralGenericComponents_after_galoisPullback
      p hD.2.2.2.2 Y hY Zc hZc F hF

instance

(anonymous instance)

L73 ↗

Source context 7 commands

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

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

Lean source · statement

instance : IsDomain (ULift.{u} ℤ)

theorem

galoisPullback_satisfiesResidueCharacteristicTwoBoundaryCondition_overIntegers

L78 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.galoisPullback_satisfiesResidueCharacteristicTwoBoundaryCondition_overIntegers

Documentation

Integer-base specialization. The structure morphism of the pullback is the unique morphism to Spec ℤ, so no extra base morphism is assumed.

Source context 8 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
open EtaleFundamentalGroups
namespace AlgebraicGeometry.Scheme.EffectiveCartierDivisor
universe u
variable {X S : Scheme.{u}}
section IntegerBase
local instance : IsDomain (ULift.{u} ℤ) :=
  (ULift.ringEquiv : ULift.{u} ℤ ≃+* ℤ).toMulEquiv.isDomain ℤ

Lean source · full declaration

theorem galoisPullback_satisfiesResidueCharacteristicTwoBoundaryCondition_overIntegers
    [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X]
    (D : EffectiveCartierDivisor X)
    (hD : D.SatisfiesResidueCharacteristicTwoBoundaryConditionOverIntegers)
    (Y : FiniteEtale X) (hY : CategoryTheory.PreGaloisCategory.IsGalois Y) :
    letI : CategoryTheory.PreGaloisCategory.IsGalois Y := hY
    letI : IsIntegral Y.left :=
      isIntegral_left_of_isConnected_finiteEtale Y
    letI : IsNormalIntegral Y.left :=
      isNormalIntegral_left_of_isConnected_finiteEtale Y
    letI : IsLocallyNoetherian Y.left :=
      isLocallyNoetherian_left_finiteEtale Y
    let D' : EffectiveCartierDivisor Y.left := D.comapFiniteEtale Y
    D'.SatisfiesResidueCharacteristicTwoBoundaryConditionOverIntegers := by
  let : CategoryTheory.PreGaloisCategory.IsGalois Y := hY
  let : IsIntegral Y.left :=
    isIntegral_left_of_isConnected_finiteEtale Y
  let : IsNormalIntegral Y.left :=
    isNormalIntegral_left_of_isConnected_finiteEtale Y
  let : IsLocallyNoetherian Y.left :=
    isLocallyNoetherian_left_finiteEtale Y
  let D' : EffectiveCartierDivisor Y.left := D.comapFiniteEtale Y
  let p : X ⟶ Spec (CommRingCat.of (ULift.{u} ℤ)) :=
    specULiftZIsTerminal.from X
  have hgeneral :=
    D.galoisPullback_satisfiesResidueCharacteristicTwoBoundaryCondition
      p hD Y hY
  dsimp only at hgeneral
  change D'.SatisfiesResidueCharacteristicTwoBoundaryCondition
    (specULiftZIsTerminal.from Y.left)
  have hp : Y.hom ≫ p = specULiftZIsTerminal.from Y.left :=
    specULiftZIsTerminal.hom_ext _ _
  rw [← hp]
  exact hgeneral

Module documentation

Arithmetic boundary stability under Galois covers

Declarations

galoisPullback_satisfiesResidueCharacteristicTwoBoundaryCondition

(anonymous instance)

galoisPullback_satisfiesResidueCharacteristicTwoBoundaryCondition_overIntegers