Module

BoundaryStrictInertia.lean

Nyll.Yamaguchi26SolvableCoverings.Geometry.BoundaryStrictInertia

8 declarations indexed from sourceView source ↗

Module documentation

Strict local inertia at a common global base point

For each boundary component we use its actual strict-Henselian generic morphism and the canonical geometric point of its fraction field. All isomorphisms from the resulting geometric fiber functor to the specified common fiber functor are included. Such paths exist on the connected complement; their induced identifications differ by inner conjugation.

The closed normal subgroup generated by these images lies in the kernel of the complement inclusion. Its finite Galois quotient criterion also recovers triviality of each local image on the entire fiber of the cover.

Imports6

Imported by2

def

boundaryStrictInertiaGenerators

L41 ↗

Yamaguchi26SolvableCoverings.boundaryStrictInertiaGenerators

Documentation

All strict generic inertia elements, transported along all geometric paths to the specified global base point.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups EtaleFundamentalGroups.Inertia
open EtaleFundamentalGroups.StrictHenselian
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]

Lean source · statement

def boundaryStrictInertiaGenerators
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (point : Spec (.of Ω) ⟶ D.1.supportComplement) : Set π₁ᵉᵗ(point)

def

boundaryStrictInertiaClosure

L54 ↗

Yamaguchi26SolvableCoverings.boundaryStrictInertiaClosure

Documentation

The closed normal subgroup generated by the manuscript's strict local inertia groups at every prime boundary component.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups EtaleFundamentalGroups.Inertia
open EtaleFundamentalGroups.StrictHenselian
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]

Lean source · statement

def boundaryStrictInertiaClosure
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (point : Spec (.of Ω) ⟶ D.1.supportComplement) : Subgroup π₁ᵉᵗ(point)

theorem

boundaryStrictInertiaGenerators_subset_kernel

L62 ↗

Yamaguchi26SolvableCoverings.boundaryStrictInertiaGenerators_subset_kernel

Documentation

Every transported local inertia element is killed by the actual inclusion homomorphism, regardless of the chosen geometric path.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups EtaleFundamentalGroups.Inertia
open EtaleFundamentalGroups.StrictHenselian
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]

Lean source · statement

theorem boundaryStrictInertiaGenerators_subset_kernel
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (point : Spec (.of Ω) ⟶ D.1.supportComplement) :
    boundaryStrictInertiaGenerators D hreg point ⊆
      (fundamentalGroupHom D.1.supportComplement.ι point).toMonoidHom.ker

theorem

boundaryStrictInertiaClosure_le_kernel

L88 ↗

Yamaguchi26SolvableCoverings.boundaryStrictInertiaClosure_le_kernel

Documentation

Taking normal generation and closure preserves inclusion in the closed kernel of the inclusion-induced fundamental-group homomorphism.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups EtaleFundamentalGroups.Inertia
open EtaleFundamentalGroups.StrictHenselian
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]

Lean source · statement

theorem boundaryStrictInertiaClosure_le_kernel
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (point : Spec (.of Ω) ⟶ D.1.supportComplement) :
    boundaryStrictInertiaClosure D hreg point ≤
      (fundamentalGroupHom D.1.supportComplement.ι point).toMonoidHom.ker

theorem

boundaryStrictInertiaClosure_eq_iInf_galoisQuotient

L102 ↗

Yamaguchi26SolvableCoverings.boundaryStrictInertiaClosure_eq_iInf_galoisQuotient

Documentation

The closed normal generation is detected by the actual pointed finite Galois quotients that kill all its generators.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups EtaleFundamentalGroups.Inertia
open EtaleFundamentalGroups.StrictHenselian
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]

Lean source · full declaration

theorem boundaryStrictInertiaClosure_eq_iInf_galoisQuotient
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
    [ConnectedSpace D.1.supportComplement]
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (point : Spec (.of Ω) ⟶ D.1.supportComplement) :
    boundaryStrictInertiaClosure D hreg point =
      ⨅ (W : FiniteEtale D.1.supportComplement) (hW : IsGalois W)
        (w : (fiber point).obj W),
        let : IsGalois W := hW
        ⨅ (_h : boundaryStrictInertiaGenerators D hreg point ⊆
          (galoisObjectQuotientMonoidHom (fiber point) π₁ᵉᵗ(point) W w).ker),
          (galoisObjectQuotientMonoidHom (fiber point) π₁ᵉᵗ(point) W w).ker :=
  topologicalClosure_normalClosure_eq_iInf_galoisQuotient
    (fiber point) (boundaryStrictInertiaGenerators D hreg point)

theorem

boundaryStrict_fiber_fixed_of_generators_subset_kernel

L120 ↗

Yamaguchi26SolvableCoverings.boundaryStrict_fiber_fixed_of_generators_subset_kernel

Documentation

A pointed Galois quotient killing the global generators has trivial local strict generic action on its entire fiber at each component. The required geometric path is obtained from connectedness of the complement.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups EtaleFundamentalGroups.Inertia
open EtaleFundamentalGroups.StrictHenselian
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]

Lean source · full declaration

theorem boundaryStrict_fiber_fixed_of_generators_subset_kernel
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
    [ConnectedSpace D.1.supportComplement]
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (point : Spec (.of Ω) ⟶ D.1.supportComplement)
    (W : FiniteEtale D.1.supportComplement) [IsGalois W]
    (w : (fiber point).obj W)
    (hs : boundaryStrictInertiaGenerators D hreg point ⊆
      (galoisObjectQuotientMonoidHom (fiber point) π₁ᵉᵗ(point) W w).ker)
    (E : Component D) :
    let : Field (boundaryStrictFractionField D E) := boundaryStrictFractionFieldField D hreg E
    let j := boundaryStrictGenericMorphism D hreg E
    let xi := boundaryStrictGenericPoint D hreg E
    ∀ (a : π₁ᵉᵗ(xi)) (y : (fiber (xi ≫ j)).obj W),
      fundamentalGroupHom j xi a • y = y := by
  intro hField j xi a y
  obtain ⟨t⟩ := nonempty_fiber_iso (xi ≫ j) point
  apply fiber_fixed_of_conj_fixed t (fundamentalGroupHom j xi a) W _ y
  intro v
  apply fiber_fixed_of_galoisObjectQuotient_eq_one (fiber point) W w _ _ v
  exact MonoidHom.mem_ker.mp (hs ⟨E, t, a, rfl⟩)

theorem

exists_boundaryStrictFiberPaths

L144 ↗

Yamaguchi26SolvableCoverings.exists_boundaryStrictFiberPaths

Documentation

One geometric path can be chosen for every boundary component because the complement is connected. No comparison is assumed as input.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups EtaleFundamentalGroups.Inertia
open EtaleFundamentalGroups.StrictHenselian
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]

Lean source · full declaration

theorem exists_boundaryStrictFiberPaths
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
    [ConnectedSpace D.1.supportComplement]
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (point : Spec (.of Ω) ⟶ D.1.supportComplement) :
    Nonempty (∀ E : Component D,
      let : Field (boundaryStrictFractionField D E) := boundaryStrictFractionFieldField D hreg E
      fiber (boundaryStrictGenericPoint D hreg E ≫ boundaryStrictGenericMorphism D hreg E) ≅
        fiber point) := by
  classical
  refine ⟨fun E => ?_⟩
  intro hField
  exact Classical.choice (nonempty_fiber_iso
    (boundaryStrictGenericPoint D hreg E ≫ boundaryStrictGenericMorphism D hreg E) point)

theorem

boundaryStrictInertiaClosure_eq_of_paths

L162 ↗

Yamaguchi26SolvableCoverings.boundaryStrictInertiaClosure_eq_of_paths

Documentation

The same closed normal subgroup is obtained by choosing just one path for each component. Every other choice differs by conjugation, already accounted for by normal generation.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups EtaleFundamentalGroups.Inertia
open EtaleFundamentalGroups.StrictHenselian
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]

Lean source · full declaration

theorem boundaryStrictInertiaClosure_eq_of_paths
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (point : Spec (.of Ω) ⟶ D.1.supportComplement)
    (paths : ∀ E : Component D,
      let : Field (boundaryStrictFractionField D E) := boundaryStrictFractionFieldField D hreg E
      fiber (boundaryStrictGenericPoint D hreg E ≫ boundaryStrictGenericMorphism D hreg E) ≅
        fiber point) :
    boundaryStrictInertiaClosure D hreg point =
      (Subgroup.normalClosure {g | ∃ E : Component D,
        let : Field (boundaryStrictFractionField D E) := boundaryStrictFractionFieldField D hreg E
        ∃ a : π₁ᵉᵗ(boundaryStrictGenericPoint D hreg E),
          continuousConjAut (paths E)
            (fundamentalGroupHom (boundaryStrictGenericMorphism D hreg E)
              (boundaryStrictGenericPoint D hreg E) a) = g}).topologicalClosure := by
  let s : Set π₁ᵉᵗ(point) := {g | ∃ E : Component D,
    let : Field (boundaryStrictFractionField D E) := boundaryStrictFractionFieldField D hreg E
    ∃ a : π₁ᵉᵗ(boundaryStrictGenericPoint D hreg E),
      continuousConjAut (paths E)
        (fundamentalGroupHom (boundaryStrictGenericMorphism D hreg E)
          (boundaryStrictGenericPoint D hreg E) a) = g}
  change boundaryStrictInertiaClosure D hreg point = (Subgroup.normalClosure s).topologicalClosure
  apply congrArg Subgroup.topologicalClosure
  apply le_antisymm
  · apply Subgroup.normalClosure_le_normal
    rintro g ⟨E, t, a, rfl⟩
    let : Field (boundaryStrictFractionField D E) := boundaryStrictFractionFieldField D hreg E
    rw [continuousConjAut_eq_conj (paths E) t]
    have ha : continuousConjAut (paths E)
        (fundamentalGroupHom (boundaryStrictGenericMorphism D hreg E)
          (boundaryStrictGenericPoint D hreg E) a) ∈ Subgroup.normalClosure s :=
      Subgroup.subset_normalClosure ⟨E, a, rfl⟩
    exact Subgroup.Normal.conj_mem inferInstance _ ha _
  · apply Subgroup.normalClosure_mono
    rintro g ⟨E, a, rfl⟩
    exact ⟨E, paths E, a, rfl⟩

Module documentation

Strict local inertia at a common global base point

Declarations