Module

CanonicalPointedMaps.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.CanonicalPointedMaps

6 declarations indexed from sourceView source ↗

Module documentation

Canonical maps with specified geometric basepoints

Transport along an equality of geometric points gives the actual pointed fundamental-group map. Its composition and identity laws follow from the canonical pullback comparisons. A map factoring through a separably closed field induces the trivial homomorphism.

Imports4

Nyll.EtaleFundamentalGroups.GeometricFiber.ArithmeticComposite
Nyll.EtaleFundamentalGroups.GeometricFiber.CanonicalPointedComposition
Nyll.EtaleFundamentalGroups.GeometricFiber.PullbackEquivalence
Mathlib.CategoryTheory.Limits.MorphismProperty

Imported by4

def

pointedFundamentalGroupHom

L32 ↗

AlgebraicGeometry.FiniteEtale.pointedFundamentalGroupHom

Documentation

The canonical fundamental-group map with an explicitly specified target point.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y Z : Scheme.{u}} {Ω : Type u} [Field Ω]

Lean source · statement

def pointedFundamentalGroupHom (f : X ⟶ Y)
    (x : Spec (.of Ω) ⟶ X) (y : Spec (.of Ω) ⟶ Y) (h : x ≫ f = y) :
    π₁ᵉᵗ(x) →ₜ* π₁ᵉᵗ(y)

theorem

pointedFundamentalGroupHom_apply

L37 ↗

AlgebraicGeometry.FiniteEtale.pointedFundamentalGroupHom_apply

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y Z : Scheme.{u}} {Ω : Type u} [Field Ω]

Lean source · statement

theorem pointedFundamentalGroupHom_apply (f : X ⟶ Y)
    (x : Spec (.of Ω) ⟶ X) (y : Spec (.of Ω) ⟶ Y) (h : x ≫ f = y)
    (a : π₁ᵉᵗ(x)) :
    pointedFundamentalGroupHom f x y h a = h ▸ fundamentalGroupHom f x a

theorem

pointedFundamentalGroupHom_comp

L45 ↗

AlgebraicGeometry.FiniteEtale.pointedFundamentalGroupHom_comp

Documentation

Composition preserves the original canonical fibre comparisons.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y Z : Scheme.{u}} {Ω : Type u} [Field Ω]

Lean source · full declaration

theorem pointedFundamentalGroupHom_comp (f : X ⟶ Y) (g : Y ⟶ Z)
    (x : Spec (.of Ω) ⟶ X) (y : Spec (.of Ω) ⟶ Y) (z : Spec (.of Ω) ⟶ Z)
    (hf : x ≫ f = y) (hg : y ≫ g = z) :
    (pointedFundamentalGroupHom g y z hg).comp
      (pointedFundamentalGroupHom f x y hf) =
    pointedFundamentalGroupHom (f ≫ g) x z
      (by rw [← Category.assoc, hf, hg]) := by
  subst y
  subst z
  apply ContinuousMonoidHom.ext
  intro a
  have h := fundamentalGroupHom_comp_of_eq f g (f ≫ g) rfl x
    (Category.assoc x f g) a
  have transport_back {a b : Spec (.of Ω) ⟶ Z} (e : a = b)
      (v : π₁ᵉᵗ(a)) (w : π₁ᵉᵗ(b)) (he : e ▸ v = w) : v = e.symm ▸ w := by
    subst b
    exact he
  exact transport_back (Category.assoc x f g) _ _ h

theorem

pointedFundamentalGroupHom_bijective

L65 ↗

AlgebraicGeometry.FiniteEtale.pointedFundamentalGroupHom_bijective

Documentation

Specifying an equal target point preserves bijectivity.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y Z : Scheme.{u}} {Ω : Type u} [Field Ω]

Lean source · statement

theorem pointedFundamentalGroupHom_bijective (f : X ⟶ Y)
    (x : Spec (.of Ω) ⟶ X) (y : Spec (.of Ω) ⟶ Y) (h : x ≫ f = y)
    (hf : Function.Bijective (fundamentalGroupHom f x)) :
    Function.Bijective (pointedFundamentalGroupHom f x y h)

theorem

pointedFundamentalGroupHom_id

L73 ↗

AlgebraicGeometry.FiniteEtale.pointedFundamentalGroupHom_id

Documentation

The canonical pointed map of the identity scheme morphism is the identity.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y Z : Scheme.{u}} {Ω : Type u} [Field Ω]

Lean source · statement

theorem pointedFundamentalGroupHom_id [ConnectedSpace X] [IsSepClosed Ω]
    (x : Spec (.of Ω) ⟶ X) :
    pointedFundamentalGroupHom (𝟙 X) x x (Category.comp_id x) =
      ContinuousMonoidHom.id π₁ᵉᵗ(x)

theorem

pointedFundamentalGroupHom_constant

L95 ↗

AlgebraicGeometry.FiniteEtale.pointedFundamentalGroupHom_constant

Documentation

A morphism factoring through a separably closed field has trivial pointed map.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y Z : Scheme.{u}} {Ω : Type u} [Field Ω]

Lean source · statement

theorem pointedFundamentalGroupHom_constant [IsSepClosed Ω]
    {K : Type u} [Field K] [IsSepClosed K]
    (f : X ⟶ Spec (.of K)) (s : Spec (.of K) ⟶ Y)
    (x : Spec (.of Ω) ⟶ X) (y : Spec (.of Ω) ⟶ Y)
    (h : x ≫ (f ≫ s) = y) :
    pointedFundamentalGroupHom (f ≫ s) x y h = 1

Module documentation

Canonical maps with specified geometric basepoints

Declarations

pointedFundamentalGroupHom

pointedFundamentalGroupHom_apply

pointedFundamentalGroupHom_comp

pointedFundamentalGroupHom_bijective

pointedFundamentalGroupHom_id

pointedFundamentalGroupHom_constant