Module

SchemeFibreEndo.lean

Nyll.AlgebraicCurves.Geometry.Schemes.SchemeFibreEndo

3 declarations indexed from sourceView source ↗

Module documentation

Scheme Fibre Endo

Imports1

Mathlib.AlgebraicGeometry.ResidueField

Imported by10

def

schemeFibreEndo

L26 ↗

AlgebraicGeometry.schemeFibreEndo

Documentation

The endomorphism induced on a scheme fibre by an endomorphism over the base.

Source context 4 commands

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

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

Lean source · statement

def schemeFibreEndo {S X : Scheme.{u}} (f : X ⟶ S) (h : X ⟶ X) (hcomm : h ≫ f = f)
    (s : S) :
    Limits.pullback f (S.fromSpecResidueField s)
      ⟶ Limits.pullback f (S.fromSpecResidueField s)

theorem

schemeFibreEndo_fst

L33 ↗

AlgebraicGeometry.schemeFibreEndo_fst

Source context 4 commands

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

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

Lean source · statement

theorem schemeFibreEndo_fst {S X : Scheme.{u}} (f : X ⟶ S) (h : X ⟶ X)
    (hcomm : h ≫ f = f) (s : S) :
    schemeFibreEndo f h hcomm s ≫ Limits.pullback.fst _ _ =
      Limits.pullback.fst _ _ ≫ h

theorem

schemeFibreEndo_snd

L39 ↗

AlgebraicGeometry.schemeFibreEndo_snd

Source context 4 commands

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

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

Lean source · statement

theorem schemeFibreEndo_snd {S X : Scheme.{u}} (f : X ⟶ S) (h : X ⟶ X)
    (hcomm : h ≫ f = f) (s : S) :
    schemeFibreEndo f h hcomm s ≫ Limits.pullback.snd _ _ = Limits.pullback.snd _ _

Module documentation

Scheme Fibre Endo

Declarations

schemeFibreEndo

schemeFibreEndo_fst

schemeFibreEndo_snd