NYLL
Module

PullbackFiberPoint.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.PullbackFiberPoint
5 declarations indexed from sourceView source ↗

Module documentation

Points in pullback fibers

The canonical comparison between a pullback fiber and a composite geometric fiber is compatible with the first projection of the scheme pullback.

Imports2
Imported by8

Declarations

instance

finiteEtaleOverCategoryPullbackFiberPoint

L25 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleOverCategoryPullbackFiberPoint
Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
Lean source · statement
instance finiteEtaleOverCategoryPullbackFiberPoint (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S)
instance

finiteEtaleHasPullbacksAlongPullbackFiberPoint

L30 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleHasPullbacksAlongPullbackFiberPoint
Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryPullbackFiberPoint (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S) :=
  instCategory S
Lean source · statement
instance finiteEtaleHasPullbacksAlongPullbackFiberPoint
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f
instance

finiteEtaleStableUnderBaseChangeAlongPullbackFiberPoint

L36 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleStableUnderBaseChangeAlongPullbackFiberPoint
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryPullbackFiberPoint (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S) :=
  instCategory S
local instance finiteEtaleHasPullbacksAlongPullbackFiberPoint
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
Lean source · statement
instance finiteEtaleStableUnderBaseChangeAlongPullbackFiberPoint
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f
theorem

pullbackFiberIso_hom_fundamentalGroupHom_apply

L47 ↗
AlgebraicGeometry.FiniteEtale.pullbackFiberIso_hom_fundamentalGroupHom_apply
Documentation

The canonical pullback-fiber comparison intertwines the action on the pulled-back fiber with the induced action on the composite fiber.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryPullbackFiberPoint (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S) :=
  instCategory S
local instance finiteEtaleHasPullbacksAlongPullbackFiberPoint
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongPullbackFiberPoint
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {X Y : Scheme.{u}} {Omega : Type u} [Field Omega]
Lean source · statement
theorem pullbackFiberIso_hom_fundamentalGroupHom_apply
    (f : X ⟶ Y) (xi : Spec (.of Omega) ⟶ X) (a : π₁ᵉᵗ(xi))
    (A : FiniteEtale Y) (y : (fiber xi).obj ((pullback f).obj A)) :
    (pullbackFiberIso f xi).hom.app A
        (a.hom.app ((pullback f).obj A) y) =
      (fundamentalGroupHom f xi a).hom.app A
        ((pullbackFiberIso f xi).hom.app A y)
theorem

pullbackFiberIso_hom_fiberObjEquivHom_left

L70 ↗
AlgebraicGeometry.FiniteEtale.pullbackFiberIso_hom_fiberObjEquivHom_left
Documentation

The pullback-fiber comparison sends a lifted point to the composite of its geometric lift with the first pullback projection.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryPullbackFiberPoint (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S) :=
  instCategory S
local instance finiteEtaleHasPullbacksAlongPullbackFiberPoint
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongPullbackFiberPoint
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {X Y : Scheme.{u}} {Omega : Type u} [Field Omega]
variable [IsSepClosed Omega]
Lean source · statement
theorem pullbackFiberIso_hom_fiberObjEquivHom_left
    (f : X ⟶ Y) (xi : Spec (.of Omega) ⟶ X)
    (A : FiniteEtale Y) (y : (fiber xi).obj ((pullback f).obj A)) :
    (fiberObjEquivHom (xi ≫ f) A ((pullbackFiberIso f xi).hom.app A y)).left =
      (fiberObjEquivHom xi ((pullback f).obj A) y).left ≫
        Limits.pullback.fst A.hom f

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