NYLL
Module

PullbackComponentQuotient.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.PullbackComponentQuotient
7 declarations indexed from sourceView source ↗

Module documentation

Quotients attached to pointed pullback components

A pointed connected Galois component of the pullback of a pointed Galois cover has the same stabilizer kernel as the restricted original quotient. The component quotient therefore induces an injective homomorphism from the component deck group to the original deck group. In particular, mapping a subgroup along this homomorphism preserves its cardinality and all numerical coprimality statements.

Imports3
Imported by3

Declarations

theorem

galoisPullbackComponent_quotient_ker_eq

L36 ↗
AlgebraicGeometry.FiniteEtale.galoisPullbackComponent_quotient_ker_eq
Documentation

The pointed quotient of a Galois pullback component and the restricted pointed quotient of the original cover have the same kernel.

Source context 7 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
Lean source · full declaration
theorem galoisPullbackComponent_quotient_ker_eq
    (f : X ⟶ Y) (xi : Spec (.of Omega) ⟶ X)
    (A : FiniteEtale Y) (hA : IsGalois A)
    (x : (fiber (xi ≫ f)).obj A)
    (Z : FiniteEtale X) (i : Z ⟶ (pullback f).obj A)
    (z : (fiber xi).obj Z)
    (hiz : (fiber xi).map i z =
      transportedPointOfCompIso (pullback f) (pullbackFiberIso f xi) A x)
    (hZ : IsGalois Z) (hi : Mono i) :
    letI : IsGalois Z := hZ
    (EtaleFundamentalGroups.finiteEtaleGaloisCoverQuotientMonoidHom
      xi Z hZ z).ker =
      (EtaleFundamentalGroups.Inertia.finiteEtaleGaloisCoverQuotientOfMorphism
        f xi A hA x).ker := by
  let : IsGalois Z := hZ
  let : Mono i := hi
  rw [EtaleFundamentalGroups.finiteEtaleGaloisCoverQuotientMonoidHom_ker,
    EtaleFundamentalGroups.Inertia.finiteEtaleGaloisCoverQuotientOfMorphism_ker]
  let y : (fiber xi).obj ((pullback f).obj A) :=
    transportedPointOfCompIso (pullback f) (pullbackFiberIso f xi) A x
  have hi_injective : Function.Injective ((fiber xi).map i) := by
    let : Mono ((fiber xi).map i) := Functor.map_mono (fiber xi) i
    exact ConcreteCategory.injective_of_mono_of_preservesPullback
      ((fiber xi).map i)
  change MulAction.stabilizer π₁ᵉᵗ(xi) z =
    MulAction.stabilizer π₁ᵉᵗ(xi) y
  ext a
  simp only [MulAction.mem_stabilizer_iff]
  constructor
  · intro ha
    calc
      a • y = a • (fiber xi).map i z :=
        congrArg (fun q ↦ a • q) hiz.symm
      _ = (fiber xi).map i (a • z) :=
        mulAction_naturality (fiber xi) a i z
      _ = (fiber xi).map i z := congrArg ((fiber xi).map i) ha
      _ = y := hiz
  · intro ha
    apply hi_injective
    calc
      (fiber xi).map i (a • z) = a • (fiber xi).map i z :=
        (mulAction_naturality (fiber xi) a i z).symm
      _ = a • y := congrArg (fun q ↦ a • q) hiz
      _ = y := ha
      _ = (fiber xi).map i z := hiz.symm
def

galoisPullbackComponentQuotientMonoidHom

L85 ↗
AlgebraicGeometry.FiniteEtale.galoisPullbackComponentQuotientMonoidHom
Documentation

The canonical deck-group homomorphism induced by a pointed Galois component of a pullback. It is characterized by composing with the surjective component quotient to give the restricted original quotient.

Source context 7 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
Lean source · statement
def galoisPullbackComponentQuotientMonoidHom
    (f : X ⟶ Y) (xi : Spec (.of Omega) ⟶ X)
    (A : FiniteEtale Y) (hA : IsGalois A)
    (x : (fiber (xi ≫ f)).obj A)
    (Z : FiniteEtale X) (i : Z ⟶ (pullback f).obj A)
    (z : (fiber xi).obj Z)
    (hiz : (fiber xi).map i z =
      transportedPointOfCompIso (pullback f) (pullbackFiberIso f xi) A x)
    (hZ : IsGalois Z) (hi : Mono i) :
    (Aut Z)ᵐᵒᵖ →* (Aut A)ᵐᵒᵖ
theorem

galoisPullbackComponentQuotientMonoidHom_comp

L109 ↗
AlgebraicGeometry.FiniteEtale.galoisPullbackComponentQuotientMonoidHom_comp
Documentation

The component-to-original deck homomorphism composes with the component quotient to give the restricted original quotient.

Source context 7 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
Lean source · full declaration
theorem galoisPullbackComponentQuotientMonoidHom_comp
    (f : X ⟶ Y) (xi : Spec (.of Omega) ⟶ X)
    (A : FiniteEtale Y) (hA : IsGalois A)
    (x : (fiber (xi ≫ f)).obj A)
    (Z : FiniteEtale X) (i : Z ⟶ (pullback f).obj A)
    (z : (fiber xi).obj Z)
    (hiz : (fiber xi).map i z =
      transportedPointOfCompIso (pullback f) (pullbackFiberIso f xi) A x)
    (hZ : IsGalois Z) (hi : Mono i) :
    letI : IsGalois Z := hZ
    (galoisPullbackComponentQuotientMonoidHom
      f xi A hA x Z i z hiz hZ hi).comp
        (EtaleFundamentalGroups.finiteEtaleGaloisCoverQuotientMonoidHom
          xi Z hZ z) =
      EtaleFundamentalGroups.Inertia.finiteEtaleGaloisCoverQuotientOfMorphism
        f xi A hA x := by
  let : IsGalois Z := hZ
  let qZ := EtaleFundamentalGroups.finiteEtaleGaloisCoverQuotientMonoidHom
    xi Z hZ z
  let qA :=
    EtaleFundamentalGroups.Inertia.finiteEtaleGaloisCoverQuotientOfMorphism
      f xi A hA x
  let hqZ :=
    EtaleFundamentalGroups.finiteEtaleGaloisCoverQuotientMonoidHom_surjective
      xi Z hZ z
  let hker : qZ.ker ≤ qA.ker :=
    (galoisPullbackComponent_quotient_ker_eq
      f xi A hA x Z i z hiz hZ hi).le
  apply MonoidHom.ext
  intro a
  exact MonoidHom.liftOfRightInverse_comp_apply
    (f := qZ) (f_inv := Function.surjInv hqZ)
    (Function.rightInverse_surjInv hqZ) ⟨qA, hker⟩ a
theorem

galoisPullbackComponentQuotientMonoidHom_injective

L145 ↗
AlgebraicGeometry.FiniteEtale.galoisPullbackComponentQuotientMonoidHom_injective
Documentation

The canonical homomorphism from component deck transformations to original deck transformations is injective.

Source context 7 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
Lean source · statement
theorem galoisPullbackComponentQuotientMonoidHom_injective
    (f : X ⟶ Y) (xi : Spec (.of Omega) ⟶ X)
    (A : FiniteEtale Y) (hA : IsGalois A)
    (x : (fiber (xi ≫ f)).obj A)
    (Z : FiniteEtale X) (i : Z ⟶ (pullback f).obj A)
    (z : (fiber xi).obj Z)
    (hiz : (fiber xi).map i z =
      transportedPointOfCompIso (pullback f) (pullbackFiberIso f xi) A x)
    (hZ : IsGalois Z) (hi : Mono i) :
    Function.Injective
      (galoisPullbackComponentQuotientMonoidHom
        f xi A hA x Z i z hiz hZ hi)
theorem

galoisPullbackComponentQuotientMonoidHom_range

L187 ↗
AlgebraicGeometry.FiniteEtale.galoisPullbackComponentQuotientMonoidHom_range
Documentation

The image of the component deck group is exactly the local-monodromy range of the original cover.

Source context 7 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
Lean source · statement
theorem galoisPullbackComponentQuotientMonoidHom_range
    (f : X ⟶ Y) (xi : Spec (.of Omega) ⟶ X)
    (A : FiniteEtale Y) (hA : IsGalois A)
    (x : (fiber (xi ≫ f)).obj A)
    (Z : FiniteEtale X) (i : Z ⟶ (pullback f).obj A)
    (z : (fiber xi).obj Z)
    (hiz : (fiber xi).map i z =
      transportedPointOfCompIso (pullback f) (pullbackFiberIso f xi) A x)
    (hZ : IsGalois Z) (hi : Mono i) :
    (galoisPullbackComponentQuotientMonoidHom
      f xi A hA x Z i z hiz hZ hi).range =
      (EtaleFundamentalGroups.Inertia.finiteEtaleGaloisCoverQuotientOfMorphism
        f xi A hA x).range
theorem

galoisPullbackComponentQuotientMonoidHom_map_natCard

L227 ↗
AlgebraicGeometry.FiniteEtale.galoisPullbackComponentQuotientMonoidHom_map_natCard
Documentation

Mapping a subgroup of the component deck group into the original deck group preserves its cardinality.

Source context 7 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
Lean source · statement
theorem galoisPullbackComponentQuotientMonoidHom_map_natCard
    (f : X ⟶ Y) (xi : Spec (.of Omega) ⟶ X)
    (A : FiniteEtale Y) (hA : IsGalois A)
    (x : (fiber (xi ≫ f)).obj A)
    (Z : FiniteEtale X) (i : Z ⟶ (pullback f).obj A)
    (z : (fiber xi).obj Z)
    (hiz : (fiber xi).map i z =
      transportedPointOfCompIso (pullback f) (pullbackFiberIso f xi) A x)
    (hZ : IsGalois Z) (hi : Mono i)
    (H : Subgroup (Aut Z)ᵐᵒᵖ) :
    Nat.card (H.map (galoisPullbackComponentQuotientMonoidHom
      f xi A hA x Z i z hiz hZ hi)) = Nat.card H
theorem

galoisPullbackComponentQuotientMonoidHom_map_coprime_iff

L245 ↗
AlgebraicGeometry.FiniteEtale.galoisPullbackComponentQuotientMonoidHom_map_coprime_iff
Documentation

Coprimality of a component deck subgroup is unchanged after mapping it to the original deck group.

Source context 7 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
Lean source · statement
theorem galoisPullbackComponentQuotientMonoidHom_map_coprime_iff
    (f : X ⟶ Y) (xi : Spec (.of Omega) ⟶ X)
    (A : FiniteEtale Y) (hA : IsGalois A)
    (x : (fiber (xi ≫ f)).obj A)
    (Z : FiniteEtale X) (i : Z ⟶ (pullback f).obj A)
    (z : (fiber xi).obj Z)
    (hiz : (fiber xi).map i z =
      transportedPointOfCompIso (pullback f) (pullbackFiberIso f xi) A x)
    (hZ : IsGalois Z) (hi : Mono i)
    (H : Subgroup (Aut Z)ᵐᵒᵖ) (n : ℕ) :
    Nat.Coprime
        (Nat.card (H.map (galoisPullbackComponentQuotientMonoidHom
          f xi A hA x Z i z hiz hZ hi))) n ↔
      Nat.Coprime (Nat.card H) n

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