NYLL
Module

DivisorialFiniteImageCoprimality.lean

Nyll.EtaleFundamentalGroups.Inertia.DivisorialFiniteImageCoprimality
4 declarations indexed from sourceView source ↗

Module documentation

Coprimality transfer for divisorial finite images

The image of a geometric local fundamental group in a pointed finite Galois quotient is a finite subgroup of the deck group. Its order therefore divides the deck-group order, and more sharply divides the order of every subgroup which contains that image.

Imports2
Imported by1

Declarations

theorem

finiteEtaleGaloisCoverQuotient_map_fundamentalGroupImage_natCard_dvd_aut

L30 ↗
EtaleFundamentalGroups.Inertia.finiteEtaleGaloisCoverQuotient_map_fundamentalGroupImage_natCard_dvd_aut
Documentation

The finite monodromy image contributed by a geometric source has order dividing the automorphism-group order of the pointed Galois cover.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u
Lean source · full declaration
theorem finiteEtaleGaloisCoverQuotient_map_fundamentalGroupImage_natCard_dvd_aut
    {T U : Scheme.{u}} [ConnectedSpace U]
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (j : T ⟶ U) (xi : Spec (.of Omega) ⟶ T)
    (Y : FiniteEtale U) (hY : IsGalois Y)
    (y : (FiniteEtale.fiber (xi ≫ j)).obj Y) :
    letI : IsGalois Y := hY
    Nat.card
        (Subgroup.map
          (finiteEtaleGaloisCoverQuotientMonoidHom
            (xi ≫ j) Y hY y)
          (fundamentalGroupImageOfMorphism j xi)) ∣
      Nat.card (Aut Y) := by
  let : IsGalois Y := hY
  rw [finiteEtaleGaloisCoverQuotient_map_fundamentalGroupImage]
  calc
    Nat.card
          (finiteEtaleGaloisCoverQuotientOfMorphism
            j xi Y hY y).range ∣
        Nat.card ((Aut Y)ᵐᵒᵖ) :=
      Subgroup.card_subgroup_dvd_card
        (finiteEtaleGaloisCoverQuotientOfMorphism j xi Y hY y).range
    _ = Nat.card (Aut Y) :=
      Nat.card_congr MulOpposite.opEquiv.symm
theorem

finiteEtaleGaloisCoverQuotient_map_fundamentalGroupImage_natCard_dvd_of_le

L57 ↗
EtaleFundamentalGroups.Inertia.finiteEtaleGaloisCoverQuotient_map_fundamentalGroupImage_natCard_dvd_of_le
Documentation

If the geometric-source finite image lies in a specified subgroup of the deck group, its order divides the order of that subgroup.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u
Lean source · full declaration
theorem finiteEtaleGaloisCoverQuotient_map_fundamentalGroupImage_natCard_dvd_of_le
    {T U : Scheme.{u}} [ConnectedSpace U]
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (j : T ⟶ U) (xi : Spec (.of Omega) ⟶ T)
    (Y : FiniteEtale U) (hY : IsGalois Y)
    (y : (FiniteEtale.fiber (xi ≫ j)).obj Y)
    (H : Subgroup (Aut Y)ᵐᵒᵖ)
    (himage :
      Subgroup.map
          (finiteEtaleGaloisCoverQuotientMonoidHom
            (xi ≫ j) Y hY y)
          (fundamentalGroupImageOfMorphism j xi) ≤ H) :
    letI : IsGalois Y := hY
    Nat.card
        (Subgroup.map
          (finiteEtaleGaloisCoverQuotientMonoidHom
            (xi ≫ j) Y hY y)
          (fundamentalGroupImageOfMorphism j xi)) ∣
      Nat.card H := by
  let : IsGalois Y := hY
  exact Subgroup.card_dvd_of_le himage
theorem

finiteEtaleGaloisCoverQuotient_map_fundamentalGroupImage_coprime_of_le

L81 ↗
EtaleFundamentalGroups.Inertia.finiteEtaleGaloisCoverQuotient_map_fundamentalGroupImage_coprime_of_le
Documentation

Coprimality of a containing finite subgroup descends to the geometric local monodromy image.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u
Lean source · full declaration
theorem finiteEtaleGaloisCoverQuotient_map_fundamentalGroupImage_coprime_of_le
    {T U : Scheme.{u}} [ConnectedSpace U]
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (j : T ⟶ U) (xi : Spec (.of Omega) ⟶ T)
    (Y : FiniteEtale U) (hY : IsGalois Y)
    (y : (FiniteEtale.fiber (xi ≫ j)).obj Y)
    (H : Subgroup (Aut Y)ᵐᵒᵖ)
    (himage :
      Subgroup.map
          (finiteEtaleGaloisCoverQuotientMonoidHom
            (xi ≫ j) Y hY y)
          (fundamentalGroupImageOfMorphism j xi) ≤ H)
    (p : ℕ) (hcoprime : Nat.Coprime (Nat.card H) p) :
    letI : IsGalois Y := hY
    Nat.Coprime
      (Nat.card
        (Subgroup.map
          (finiteEtaleGaloisCoverQuotientMonoidHom
            (xi ≫ j) Y hY y)
          (fundamentalGroupImageOfMorphism j xi))) p := by
  let : IsGalois Y := hY
  exact hcoprime.of_dvd_left
    (finiteEtaleGaloisCoverQuotient_map_fundamentalGroupImage_natCard_dvd_of_le
      j xi Y hY y H himage)
theorem

finiteEtaleGaloisCoverQuotient_map_fundamentalGroupImage_coprime_of_aut

L108 ↗
EtaleFundamentalGroups.Inertia.finiteEtaleGaloisCoverQuotient_map_fundamentalGroupImage_coprime_of_aut
Documentation

In particular, coprimality of the whole component deck group descends to the geometric local monodromy image.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u
Lean source · full declaration
theorem finiteEtaleGaloisCoverQuotient_map_fundamentalGroupImage_coprime_of_aut
    {T U : Scheme.{u}} [ConnectedSpace U]
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (j : T ⟶ U) (xi : Spec (.of Omega) ⟶ T)
    (Y : FiniteEtale U) (hY : IsGalois Y)
    (y : (FiniteEtale.fiber (xi ≫ j)).obj Y)
    (p : ℕ) (hcoprime : Nat.Coprime (Nat.card (Aut Y)) p) :
    letI : IsGalois Y := hY
    Nat.Coprime
      (Nat.card
        (Subgroup.map
          (finiteEtaleGaloisCoverQuotientMonoidHom
            (xi ≫ j) Y hY y)
          (fundamentalGroupImageOfMorphism j xi))) p := by
  let : IsGalois Y := hY
  exact hcoprime.of_dvd_left
    (finiteEtaleGaloisCoverQuotient_map_fundamentalGroupImage_natCard_dvd_aut
      j xi Y hY y)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.