Module

PointSections.lean

Nyll.SchemeTheory.FiniteEtale.PointSections

10 declarations indexed from sourceView source ↗

Module documentation

Points and sections of finite étale covers over a ring

The canonical affine presentation and the native spectrum algebra-hom equivalence identify points with algebra maps on sections over any base ring. The comparison is natural and respects actual point automorphisms.

Imports4

Nyll.SchemeTheory.Pi1.FiniteEtale.Geometry
Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.RingTheory.RingHom.Finite

Imported by2

theorem

sectionsScalarMap_eq

L31 ↗

AlgebraicGeometry.FiniteEtale.sectionsScalarMap_eq

Documentation

The existing section algebra has the literal affine structure 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 (H : Type u) [CommRing H]

Lean source · statement

theorem sectionsScalarMap_eq (X : FiniteEtale (Spec (.of H))) :
    CommRingCat.ofHom (algebraMap H Γ(X.left, ⊤)) =
      (Scheme.ΓSpecIso (.of H)).inv ≫ X.hom.appTop

theorem

sections_moduleFinite

L41 ↗

AlgebraicGeometry.FiniteEtale.sections_moduleFinite

Documentation

Finiteness of the actual scheme morphism gives finite sections over the original ring, with the existing section-algebra structure.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (H : Type u) [CommRing H]

Lean source · statement

theorem sections_moduleFinite (X : FiniteEtale (Spec (.of H))) :
    Module.Finite H Γ(X.left, ⊤)

theorem

isoSpec_over

L56 ↗

AlgebraicGeometry.FiniteEtale.isoSpec_over

Documentation

The canonical affine presentation lies over the original base ring.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (H : Type u) [CommRing H]

Lean source · statement

theorem isoSpec_over (X : FiniteEtale (Spec (.of H))) :
    X.left.isoSpec.hom ≫ Spec.algebraMap H Γ(X.left, ⊤) = X.hom

def

sectionsAlgHom

L68 ↗

AlgebraicGeometry.FiniteEtale.sectionsAlgHom

Documentation

Restriction of sections along an actual finite étale-cover morphism.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (H : Type u) [CommRing H]

Lean source · full declaration

def sectionsAlgHom {X Y : FiniteEtale (Spec (.of H))} (f : X ⟶ Y) :
    Γ(Y.left, ⊤) →ₐ[H] Γ(X.left, ⊤) where
  __ := f.left.appTop.hom
  commutes' h := by
    have : f.left.IsOver (Spec (.of H)) := ⟨MorphismProperty.Over.w f⟩
    have hLE := appLE_comp_algebraMap f.left H ⊤ ⊤ le_rfl
    have hTop : f.left.appTop.hom.comp (algebraMap H Γ(Y.left, ⊤)) =
        algebraMap H Γ(X.left, ⊤) :=
      (congrArg (fun k : Γ(Y.left, ⊤) ⟶ Γ(X.left, ⊤) =>
        k.hom.comp (algebraMap H Γ(Y.left, ⊤)))
          (Scheme.Hom.app_eq_appLE f.left)).trans hLE
    exact RingHom.congr_fun hTop h

def

pointHomSpecEquiv

L83 ↗

AlgebraicGeometry.FiniteEtale.pointHomSpecEquiv

Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (H : Type u) [CommRing H]
variable (Ω : Type u) [CommRing Ω] [Algebra H Ω]

Lean source · full declaration

def pointHomSpecEquiv (X : FiniteEtale (Spec (.of H))) :
    (Over.mk (Spec.algebraMap H Ω) ⟶ X.toComma) ≃
      {f : Spec (.of Ω) ⟶ Spec Γ(X.left, ⊤) //
        f ≫ Spec.algebraMap H Γ(X.left, ⊤) = Spec.algebraMap H Ω} where
  toFun x := ⟨x.left ≫ X.left.isoSpec.hom,
    (Category.assoc _ _ _).trans
      ((congrArg (fun k : X.left ⟶ Spec (.of H) => x.left ≫ k)
        (isoSpec_over H X)).trans x.w)⟩
  invFun x := Over.homMk (x.val ≫ X.left.isoSpec.inv) (by
    have hInv : X.left.isoSpec.inv ≫ X.hom = Spec.algebraMap H Γ(X.left, ⊤) :=
      (congrArg (fun k : X.left ⟶ Spec (.of H) => X.left.isoSpec.inv ≫ k)
        (isoSpec_over H X).symm).trans (Iso.inv_hom_id_assoc _ _)
    exact (Category.assoc _ _ _).trans
      ((congrArg (fun k : Spec Γ(X.left, ⊤) ⟶ Spec (.of H) => x.val ≫ k) hInv).trans
        x.property))
  left_inv x := by
    apply Over.OverMorphism.ext
    change (x.left ≫ X.left.isoSpec.hom) ≫ X.left.isoSpec.inv = x.left
    simp only [Category.assoc, Iso.hom_inv_id, Category.comp_id]
  right_inv x := by
    apply Subtype.ext
    change (x.val ≫ X.left.isoSpec.inv) ≫ X.left.isoSpec.hom = x.val
    simp only [Category.assoc, Iso.inv_hom_id, Category.comp_id]

def

pointHomAlgEquiv

L108 ↗

AlgebraicGeometry.FiniteEtale.pointHomAlgEquiv

Documentation

The actual over-point/section-algebra correspondence over a ring base.

Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (H : Type u) [CommRing H]
variable (Ω : Type u) [CommRing Ω] [Algebra H Ω]

Lean source · statement

def pointHomAlgEquiv (X : FiniteEtale (Spec (.of H))) :
    (Over.mk (Spec.algebraMap H Ω) ⟶ X.toComma) ≃ (Γ(X.left, ⊤) →ₐ[H] Ω)

theorem

pointHomAlgEquiv_specMap

L113 ↗

AlgebraicGeometry.FiniteEtale.pointHomAlgEquiv_specMap

Documentation

The inverse spectrum computation retains the actual point morphism.

Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (H : Type u) [CommRing H]
variable (Ω : Type u) [CommRing Ω] [Algebra H Ω]

Lean source · statement

theorem pointHomAlgEquiv_specMap (X : FiniteEtale (Spec (.of H)))
    (x : Over.mk (Spec.algebraMap H Ω) ⟶ X.toComma) :
    Spec.map (CommRingCat.ofHom (pointHomAlgEquiv H Ω X x).toRingHom) =
      x.left ≫ X.left.isoSpec.hom

theorem

pointHomAlgEquiv_naturality

L122 ↗

AlgebraicGeometry.FiniteEtale.pointHomAlgEquiv_naturality

Documentation

The section correspondence commutes with actual cover morphisms.

Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (H : Type u) [CommRing H]
variable (Ω : Type u) [CommRing Ω] [Algebra H Ω]

Lean source · statement

theorem pointHomAlgEquiv_naturality {X Y : FiniteEtale (Spec (.of H))}
    (f : X ⟶ Y) (x : Over.mk (Spec.algebraMap H Ω) ⟶ X.toComma) :
    pointHomAlgEquiv H Ω Y (x ≫ f.hom) =
      (pointHomAlgEquiv H Ω X x).comp (sectionsAlgHom H f)

def

mapPointHom

L153 ↗

AlgebraicGeometry.FiniteEtale.mapPointHom

Documentation

The actual action of a base-linear field automorphism on over-points.

Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (H : Type u) [CommRing H]
variable (Ω : Type u) [CommRing Ω] [Algebra H Ω]

Lean source · statement

def mapPointHom (σ : Ω ≃ₐ[H] Ω) (X : FiniteEtale (Spec (.of H)))
    (x : Over.mk (Spec.algebraMap H Ω) ⟶ X.toComma) :
    Over.mk (Spec.algebraMap H Ω) ⟶ X.toComma

theorem

pointHomAlgEquiv_mapPointHom

L168 ↗

AlgebraicGeometry.FiniteEtale.pointHomAlgEquiv_mapPointHom

Documentation

The same point action is postcomposition on its section-algebra map.

Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (H : Type u) [CommRing H]
variable (Ω : Type u) [CommRing Ω] [Algebra H Ω]

Lean source · statement

theorem pointHomAlgEquiv_mapPointHom (σ : Ω ≃ₐ[H] Ω)
    (X : FiniteEtale (Spec (.of H))) (x : Over.mk (Spec.algebraMap H Ω) ⟶ X.toComma) :
    pointHomAlgEquiv H Ω X (mapPointHom H Ω σ X x) =
      σ.toAlgHom.comp (pointHomAlgEquiv H Ω X x)

Module documentation

Points and sections of finite étale covers over a ring

Declarations