NYLL
Module

OpenCoverInvariants.lean

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

Module documentation

Degree and nonempty boundary of actual open covers

Imports3
Imported by2

Declarations

theorem

openBoundary_nonempty_of_finite_square

L24 ↗
EtaleFundamentalGroups.openBoundary_nonempty_of_finite_square
Documentation

The actual finite extension has a place above every omitted place, so the source of the open cover still has nonempty boundary.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups
attribute [local instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smooth
Lean source · statement
theorem openBoundary_nonempty_of_finite_square
    {K F E : Type} [Field K] [IsAlgClosed K] [CharZero K]
    [Field F] [Field E] [Algebra K F] [Algebra K E]
    (M : CurveModel K F) (N : CurveModel K E)
    (d : N.C ⟶ M.C) (hd : d ≫ M.toBase = N.toBase)
    [IsFinite d] (hsurj : Function.Surjective d)
    {X Y : Scheme} (j : X ⟶ M.C) (k : Y ⟶ N.C)
    (hboundary : ∀ y : N.C, y ∉ Set.range k ↔ d y ∉ Set.range j)
    (hS : (M.openBoundaryPlaces j).Nonempty) :
    (N.openBoundaryPlaces k).Nonempty
theorem

one_lt_functionField_degree_of_nontrivial_galois_deck

L52 ↗
EtaleFundamentalGroups.one_lt_functionField_degree_of_nontrivial_galois_deck
Documentation

A nonidentity actual Galois deck transformation forces the actual function-field degree to be greater than one.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups
attribute [local instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smooth
Lean source · full declaration
theorem one_lt_functionField_degree_of_nontrivial_galois_deck
    {X : Scheme} [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X]
    (W : FiniteEtale X) [IsGalois W] (σ : Aut W) (hσ : σ ≠ 1) :
    let : IsIntegral W.left := isIntegral_left_of_isConnected_finiteEtale W
    let : Algebra X.functionField W.left.functionField := finiteEtaleFunctionFieldAlgebra W
    1 < Module.finrank X.functionField W.left.functionField := by
  intro hIntegral algW
  rw [← natCard_finiteEtaleAut_eq_finrank_functionField_of_isGalois W inferInstance]
  by_contra h
  have hc : Nat.card (Aut W) = 1 :=
    Nat.le_antisymm (Nat.le_of_not_gt h) (Nat.succ_le_of_lt Nat.card_pos)
  have hs := (Nat.card_eq_one_iff_unique.mp hc).1
  exact hσ (hs.elim σ 1)

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