Module

GaloisPullbackConclusions.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.Boundary.GaloisPullbackConclusions

3 declarations indexed from sourceView source ↗

Module documentation

Arithmetic-boundary conclusions for Galois pullbacks

The declarations in this module are the categorical Galois-cover layer over the general finite étale divisor lemmas in SchemeTheory.

Imports2

Imported by2

lemma

regularAlong_and_geometricallyIntegralGenericComponents_of_galoisPullback

L35 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.regularAlong_and_geometricallyIntegralGenericComponents_of_galoisPullback

Documentation

The regularity and geometric-integrality conclusions of finite-etale boundary stability. Both are obtained from the stated boundary condition: regularity ascends etale-locally, while geometric integrality is clause (ii) evaluated on the given Galois cover.

Source context 7 commands

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

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

Lean source · statement

lemma regularAlong_and_geometricallyIntegralGenericComponents_of_galoisPullback
    [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') :
    (D.1.comap Y'.hom).IsAmbientRegularAlongSupport ∧
      ∀ (Z : Set (D.1.comap Y'.hom).subscheme)
        (hZ : Z ∈ irreducibleComponents (D.1.comap Y'.hom).subscheme),
        GeometricallyIntegral
          ((D.pulledBackComponentToBase p Y' Z hZ).fiberToSpecResidueField
            (genericPoint S))

lemma

galoisPullback_regularAlong_and_componentConclusions

L56 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.galoisPullback_regularAlong_and_componentConclusions

Documentation

For a connected finite-etale Galois pullback, the ambient scheme is regular along the pulled-back boundary, and every pulled-back component has geometrically integral generic fibre together with a residue-characteristic two point where the pulled-back boundary has normal crossings.

Source context 7 commands

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

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

Lean source · statement

lemma galoisPullback_regularAlong_and_componentConclusions
    [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') :
    (D.1.comap Y'.hom).IsAmbientRegularAlongSupport ∧
      ∀ (Z : Set (D.1.comap Y'.hom).subscheme)
        (hZ : Z ∈ irreducibleComponents (D.1.comap Y'.hom).subscheme),
        GeometricallyIntegral
            ((D.pulledBackComponentToBase p Y' Z hZ).fiberToSpecResidueField
              (genericPoint S)) ∧
          ∃ y : (D.1.comap Y'.hom).subscheme,
            y ∈ Z ∧
              ringChar (Y'.left.residueField
                ((D.1.comap Y'.hom).subschemeι y)) = 2 ∧
                (D.1.comap Y'.hom).IsNormalCrossingsAt
                  ((D.1.comap Y'.hom).subschemeι y)

lemma

galoisPullback_regularAlong_and_componentConclusions_overIntegers

L84 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.galoisPullback_regularAlong_and_componentConclusions_overIntegers

Documentation

Integer-base specialization of the finite-etale Galois pullback conclusions. The structure morphism is the canonical map to the terminal scheme Spec ℤ, rather than additional input data.

Source context 7 commands

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

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

Lean source · full declaration

lemma galoisPullback_regularAlong_and_componentConclusions_overIntegers
    [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X]
    (D : EffectiveCartierDivisor X)
    (hD : D.SatisfiesResidueCharacteristicTwoBoundaryConditionOverIntegers)
    (Y' : FiniteEtale X) (hY' : CategoryTheory.PreGaloisCategory.IsGalois Y') :
    letI : IsDomain (ULift.{u} ℤ) :=
      (ULift.ringEquiv : ULift.{u} ℤ ≃+* ℤ).toMulEquiv.isDomain ℤ
    (D.1.comap Y'.hom).IsAmbientRegularAlongSupport ∧
      ∀ (Z : Set (D.1.comap Y'.hom).subscheme)
        (hZ : Z ∈ irreducibleComponents (D.1.comap Y'.hom).subscheme),
        GeometricallyIntegral
            ((D.pulledBackComponentToBase
                (specULiftZIsTerminal.from X) Y' Z hZ).fiberToSpecResidueField
              (genericPoint (Spec (CommRingCat.of (ULift.{u} ℤ))))) ∧
          ∃ y : (D.1.comap Y'.hom).subscheme,
            y ∈ Z ∧
              ringChar (Y'.left.residueField
                ((D.1.comap Y'.hom).subschemeι y)) = 2 ∧
                (D.1.comap Y'.hom).IsNormalCrossingsAt
                  ((D.1.comap Y'.hom).subschemeι y) := by
  let : IsDomain (ULift.{u} ℤ) :=
    (ULift.ringEquiv : ULift.{u} ℤ ≃+* ℤ).toMulEquiv.isDomain ℤ
  apply galoisPullback_regularAlong_and_componentConclusions D
    (specULiftZIsTerminal.from X) _ Y' hY'
  exact hD

Module documentation

Arithmetic-boundary conclusions for Galois pullbacks

Declarations

regularAlong_and_geometricallyIntegralGenericComponents_of_galoisPullback

galoisPullback_regularAlong_and_componentConclusions

galoisPullback_regularAlong_and_componentConclusions_overIntegers