NYLL
Module

DoubleCoverQuotient.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.DoubleCoverQuotient
2 declarations indexed from sourceView source ↗

Module documentation

The cyclic quotient supplied by a connected double cover

The action of the fundamental group on a connected two-element fiber is transitive. A point stabilizer therefore has index two and is normal. The stabilizer is open for the actual fiber-functor topology, so its quotient is discrete. Identifying this two-element quotient with the cyclic group constructs a continuous surjection; Galoisness or a quotient map is not an additional input.

Imports11
Imported by2

Declarations

theorem

exists_surjective_cyclicTwo_of_connected_fiber_card_two

L40 ↗
CategoryTheory.PreGaloisCategory.exists_surjective_cyclicTwo_of_connected_fiber_card_two
Documentation

A connected object with two-element fiber gives a continuous cyclic quotient of order two of the automorphism group of the fiber functor.

Source context 4 commands

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

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
universe u v w
Lean source · statement
theorem exists_surjective_cyclicTwo_of_connected_fiber_card_two
    {C : Type u} [Category.{v} C] [GaloisCategory C]
    (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
    (X : C) [IsConnected X] (hcard : Nat.card (F.obj X) = 2) :
    ∃ φ : Aut F →ₜ* Multiplicative (ZMod 2), Function.Surjective φ
theorem

exists_surjective_cyclicTwo_of_connected_doubleCover

L75 ↗
AlgebraicGeometry.FiniteEtale.exists_surjective_cyclicTwo_of_connected_doubleCover
Documentation

A connected finite etale cover of degree two constructs a continuous surjection from the actual etale fundamental group to the cyclic group of order two. Its degree is measured at the given geometric point.

Source context 4 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem exists_surjective_cyclicTwo_of_connected_doubleCover
    {S : Scheme.{u}} [ConnectedSpace S]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (.of Ω) ⟶ S) (Y : FiniteEtale S) [ConnectedSpace Y.left]
    (hdegree : Y.hom.finrank (ξ (IsLocalRing.closedPoint Ω)) = 2) :
    ∃ φ : π₁ᵉᵗ(ξ) →ₜ* Multiplicative (ZMod 2), Function.Surjective φ

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