NYLL
Module

ProperKunneth.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.ProperKunneth
6 declarations indexed from sourceView source ↗

Module documentation

The pointed proper Künneth comparison

For a proper smooth geometrically connected scheme over a separably closed field and a connected locally Noetherian second factor, the actual pair of projection homomorphisms is an isomorphism on fundamental groups at any rational basepoint. The proof identifies the rational fibre with the first factor and applies the proper homotopy sequence to the second projection.

Imports7
Imported by2

Declarations

theorem

pair_bijective_of_exact

L34 ↗
AlgebraicGeometry.FiniteEtale.pair_bijective_of_exact
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits
open AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_isReduced_of_isReduced_of_isLocallyNoetherian
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem pair_bijective_of_exact
    {D H B C : Type*} [Group D] [Group H] [Group B] [Group C]
    (i : D →* H) (p : H →* B) (q : H →* C)
    (hq : Function.Surjective q) (hexact : q.ker = i.range)
    (hpi : Function.Bijective (p.comp i)) : Function.Bijective (p.prod q)
def

rationalProductFiberIso

L69 ↗
AlgebraicGeometry.FiniteEtale.rationalProductFiberIso
Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
open AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_isReduced_of_isReduced_of_isLocallyNoetherian
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {K : Type u} [Field K] {X Y : Scheme.{u}}
Lean source · statement
def rationalProductFiberIso
    (f : X ⟶ Spec (.of K)) (g : Y ⟶ Spec (.of K))
    (y : Spec (.of K) ⟶ Y) (hy : y ≫ g = 𝟙 _) :
    Limits.pullback y (Limits.pullback.snd f g) ≅ X
theorem

pair_bijective_at_rational_fiber

L104 ↗
AlgebraicGeometry.FiniteEtale.pair_bijective_at_rational_fiber
Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
open AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_isReduced_of_isReduced_of_isLocallyNoetherian
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {K : Type u} [Field K] {X Y : Scheme.{u}}
Lean source · statement
theorem pair_bijective_at_rational_fiber
    [IsSepClosed K] [ConnectedSpace Y] [IsLocallyNoetherian Y]
    (f : X ⟶ Spec (.of K)) [IsProper f] [Smooth f] [GeometricallyConnected f]
    (g : Y ⟶ Spec (.of K))
    (y : Spec (.of K) ⟶ Y) (hy : y ≫ g = 𝟙 _)
    (xi : Spec (.of K) ⟶ Limits.pullback y (Limits.pullback.snd f g)) :
    Function.Bijective
      ((fundamentalGroupHom (Limits.pullback.fst f g)
          (xi ≫ Limits.pullback.snd y (Limits.pullback.snd f g))).prod
        (fundamentalGroupHom (Limits.pullback.snd f g)
          (xi ≫ Limits.pullback.snd y (Limits.pullback.snd f g))))
theorem

fundamentalGroupHom_proper_product_bijective

L159 ↗
AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_proper_product_bijective
Documentation

The actual pair of projection maps is bijective at a rational point of a product with a proper smooth geometrically connected first factor.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
open AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_isReduced_of_isReduced_of_isLocallyNoetherian
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {K : Type u} [Field K] {X Y : Scheme.{u}}
Lean source · statement
theorem fundamentalGroupHom_proper_product_bijective
    [IsSepClosed K] [ConnectedSpace Y] [IsLocallyNoetherian Y]
    (f : X ⟶ Spec (.of K)) [IsProper f] [Smooth f] [GeometricallyConnected f]
    (g : Y ⟶ Spec (.of K))
    (z : Spec (.of K) ⟶ Limits.pullback f g)
    (hz : (z ≫ Limits.pullback.snd f g) ≫ g = 𝟙 _) :
    Function.Bijective
      ((fundamentalGroupHom (Limits.pullback.fst f g) z).prod
        (fundamentalGroupHom (Limits.pullback.snd f g) z))
def

fundamentalGroupEquivProperProduct

L180 ↗
AlgebraicGeometry.FiniteEtale.fundamentalGroupEquivProperProduct
Documentation

The proper Künneth isomorphism has the original projection homomorphisms as its two coordinates, with their native geometric basepoints.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
open AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_isReduced_of_isReduced_of_isLocallyNoetherian
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {K : Type u} [Field K] {X Y : Scheme.{u}}
Lean source · statement
def fundamentalGroupEquivProperProduct
    [IsSepClosed K] [ConnectedSpace Y] [IsLocallyNoetherian Y]
    (f : X ⟶ Spec (.of K)) [IsProper f] [Smooth f] [GeometricallyConnected f]
    (g : Y ⟶ Spec (.of K))
    (z : Spec (.of K) ⟶ Limits.pullback f g)
    (hz : (z ≫ Limits.pullback.snd f g) ≫ g = 𝟙 _) :
    π₁ᵉᵗ(z) ≃ₜ* (π₁ᵉᵗ(z ≫ Limits.pullback.fst f g) ×
      π₁ᵉᵗ(z ≫ Limits.pullback.snd f g))
theorem

fundamentalGroupEquivProperProduct_apply

L195 ↗
AlgebraicGeometry.FiniteEtale.fundamentalGroupEquivProperProduct_apply
Documentation

The Künneth equivalence evaluates by the two actual projection maps.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
open AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_isReduced_of_isReduced_of_isLocallyNoetherian
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {K : Type u} [Field K] {X Y : Scheme.{u}}
Lean source · statement
theorem fundamentalGroupEquivProperProduct_apply
    [IsSepClosed K] [ConnectedSpace Y] [IsLocallyNoetherian Y]
    (f : X ⟶ Spec (.of K)) [IsProper f] [Smooth f] [GeometricallyConnected f]
    (g : Y ⟶ Spec (.of K))
    (z : Spec (.of K) ⟶ Limits.pullback f g)
    (hz : (z ≫ Limits.pullback.snd f g) ≫ g = 𝟙 _) (a : π₁ᵉᵗ(z)) :
    fundamentalGroupEquivProperProduct f g z hz a =
      (fundamentalGroupHom (Limits.pullback.fst f g) z a,
        fundamentalGroupHom (Limits.pullback.snd f g) z a)

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