NYLL
Module

ProperCoverSteinComparison.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.ProperCoverSteinComparison
2 declarations indexed from sourceView source ↗

Module documentation

A connected finite etale cover with a fibre section

A section over one field-valued fibre identifies a connected finite etale cover with the pullback of its native Stein factor. The section determines a point of the Stein factor by actual section descent. The connected Stein fibre over that point makes the comparison have degree one.

Imports6
Imported by2

Declarations

theorem

isIso_of_section_of_connected_source

L31 ↗
AlgebraicGeometry.FiniteEtale.isIso_of_section_of_connected_source
Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem isIso_of_section_of_connected_source
    {Y X : Scheme.{u}} (g : Y ⟶ X) [IsFiniteEtale g]
    [ConnectedSpace Y] [Nonempty X] (a : X ⟶ Y) (ha : a ≫ g = 𝟙 X) :
    IsIso g
theorem

isIso_steinComparison_of_fiber_section

L53 ↗
AlgebraicGeometry.FiniteEtale.isIso_steinComparison_of_fiber_section
Documentation

A connected finite etale cover admitting a section over one field-valued fibre is the actual pullback of its relative normalization over the base.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem isIso_steinComparison_of_fiber_section
    {Y X S : Scheme.{u}}
    (f : X ⟶ S) [IsProper f] [Flat f] [LocallyOfFinitePresentation f]
    [GeometricallyReduced f]
    [GeometricallyConnected f] (g : Y ⟶ X) [IsFiniteEtale g] [ConnectedSpace Y]
    {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ S)
    (a : Limits.pullback f s ⟶ Y) (ha : a ≫ g = Limits.pullback.fst f s) :
    IsIso (Limits.pullback.lift g (g ≫ f).toNormalization
      (g ≫ f).toNormalization_fromNormalization.symm)

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