Module

GaloisGenericComponents.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.Boundary.GaloisGenericComponents

4 declarations indexed from sourceView source ↗

Module documentation

Geometric generic boundary components in finite-etale towers

The geometric-integrality clause for boundary components after Galois finite-etale covers is inherited after a connected Galois pullback. The proof dominates a composite cover by a Galois cover of the original base and descends geometric integrality along a finite surjective morphism of reduced irreducible components.

Imports4

Nyll.EtaleFundamentalGroups.FiniteEtale.Boundary.ArithmeticCondition
Nyll.SchemeTheory.Divisors.IrreducibleComponentMap
Nyll.EtaleFundamentalGroups.FiniteEtale.GaloisDomination
Mathlib.AlgebraicGeometry.PullbackCarrier

Imported by2

lemma

geometricallyIntegral_component_of_galois_domination

L37 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.geometricallyIntegral_component_of_galois_domination

Documentation

Geometric integrality of a boundary component descends from a Galois cover dominating the given finite-etale cover.

Source context 7 commands

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

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

Lean source · statement

lemma geometricallyIntegral_component_of_galois_domination
    [IsIntegral X] [IsIntegral S]
    (D : EffectiveCartierDivisor X) (p : X ⟶ S)
    (hD : D.HasGeometricallyIntegralGenericComponentsAfterGaloisCovers p)
    (W A : FiniteEtale X) [ConnectedSpace W.left]
    (a : A ⟶ W) (hA : IsGalois A)
    (F : Set (D.1.comap W.hom).subscheme)
    (hF : F ∈ irreducibleComponents (D.1.comap W.hom).subscheme) :
    GeometricallyIntegral
      (((D.1.comap W.hom).componentToBase (W.hom ≫ p) F hF).fiberToSpecResidueField
        (genericPoint S))

lemma

geometricallyIntegralGenericComponents_after_galois_tower

L100 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.geometricallyIntegralGenericComponents_after_galois_tower

Documentation

In a two-stage connected finite-etale tower, geometric integrality of every generic boundary component follows from the Galois-cover clause on the original base.

Source context 7 commands

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

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

Lean source · statement

lemma geometricallyIntegralGenericComponents_after_galois_tower
    [IsIntegral X] [IsIntegral S]
    (D : EffectiveCartierDivisor X) (p : X ⟶ S)
    (hD : D.HasGeometricallyIntegralGenericComponentsAfterGaloisCovers p)
    (Y : FiniteEtale X) [ConnectedSpace Y.left]
    (Zc : FiniteEtale Y.left) (hZc : IsGalois Zc)
    (F : Set ((D.1.comap Y.hom).comap Zc.hom).subscheme)
    (hF : F ∈ irreducibleComponents
      ((D.1.comap Y.hom).comap Zc.hom).subscheme) :
    GeometricallyIntegral
      ((((D.1.comap Y.hom).comap Zc.hom).componentToBase
        ((Zc.hom ≫ Y.hom) ≫ p) F hF).fiberToSpecResidueField
          (genericPoint S))

theorem

connectedSpaceLeftOfIsGalois

L139 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.connectedSpaceLeftOfIsGalois

Source context 7 commands

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

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

Lean source · statement

theorem connectedSpaceLeftOfIsGalois [ConnectedSpace X]
    (Y : FiniteEtale X) (hY : IsGalois Y) : ConnectedSpace Y.left

lemma

geometricallyIntegralGenericComponents_after_galoisPullback

L146 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.geometricallyIntegralGenericComponents_after_galoisPullback

Documentation

The geometric-integrality clause on all connected Galois covers is inherited by a connected finite-etale Galois pullback.

Source context 7 commands

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

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

Lean source · full declaration

lemma geometricallyIntegralGenericComponents_after_galoisPullback
    [IsIntegral X] [IsIntegral S]
    (D : EffectiveCartierDivisor X) (p : X ⟶ S)
    (hD : D.HasGeometricallyIntegralGenericComponentsAfterGaloisCovers p)
    (Y : FiniteEtale X) (hY : IsGalois Y) :
    letI : ConnectedSpace Y.left := connectedSpaceLeftOfIsGalois Y hY
    ∀ (Zc : FiniteEtale Y.left), IsGalois Zc →
      ∀ (F : Set ((D.1.comap Y.hom).comap Zc.hom).subscheme)
        (hF : F ∈ irreducibleComponents
          ((D.1.comap Y.hom).comap Zc.hom).subscheme),
        GeometricallyIntegral
          ((((D.1.comap Y.hom).comap Zc.hom).componentToBase
            ((Zc.hom ≫ Y.hom) ≫ p) F hF).fiberToSpecResidueField
              (genericPoint S)) :=
  @geometricallyIntegralGenericComponents_after_galois_tower
    X S _ _ D p hD Y (connectedSpaceLeftOfIsGalois Y hY)

Module documentation

Geometric generic boundary components in finite-etale towers

Declarations

geometricallyIntegral_component_of_galois_domination

geometricallyIntegralGenericComponents_after_galois_tower

connectedSpaceLeftOfIsGalois

geometricallyIntegralGenericComponents_after_galoisPullback