Module

ArithmeticExact.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.ArithmeticExact

1 declaration indexed from sourceView source ↗

Module documentation

Arithmetic Exact

Exactness at the middle fundamental group for the separable constant extension of a qcqs scheme whose geometric base change is connected.

Imports7

Imported by4

theorem

fundamentalGroupHom_constantField_ker_eq_range

L28 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_constantField_ker_eq_range

Documentation

Exactness at the middle fundamental group for the separable constant extension of a qcqs scheme whose geometric base change is connected.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits CategoryTheory.PreGaloisCategory
universe u
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

theorem fundamentalGroupHom_constantField_ker_eq_range
    (k L : Type u) [Field k] [Field L] [Algebra k L]
    [Algebra.IsSeparable k L] [IsSepClosed L]
    {X : Scheme.{u}} [CompactSpace X] [QuasiSeparatedSpace X]
    (f : X ⟶ Spec (.of k))
    [ConnectedSpace ↑(Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (xi : Spec (.of Ω) ⟶ Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f) :
    (fundamentalGroupHom f (xi ≫ Limits.pullback.snd _ f)).toMonoidHom.ker =
      (fundamentalGroupHom (Limits.pullback.snd _ f) xi).toMonoidHom.range

Module documentation

Arithmetic Exact

Declarations

fundamentalGroupHom_constantField_ker_eq_range