Module

GermToFunctionField_app_eq_of_fromSpecStalk_comp_eq.lean

Nyll.AlgebraicCurves.Models.GermToFunctionField_app_eq_of_fromSpecStalk_comp_eq

2 declarations indexed from sourceView source ↗

Module documentation

Germ To Function Field app eq of from Spec Stalk comp eq

Imports11

Mathlib.AlgebraicGeometry.FunctionField
Mathlib.AlgebraicGeometry.Stalk
Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Mathlib.AlgebraicGeometry.Scheme
Mathlib.AlgebraicGeometry.Properties
Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Mathlib.Topology.Sheaves.Stalks
Mathlib.Topology.Sober
Mathlib.Algebra.Category.Ring.Basic
Mathlib.Algebra.Ring.Hom.Defs
Mathlib.CategoryTheory.Category.Basic

Imported by3

theorem

comp_algebraMap_stalk_eq

L41 ↗

AlgebraicCurves.Models.Proofs.GermToFunctionField_app_eq_of_fromSpecStalk_comp_eq.AlgebraicCurve.GlueAux.comp_algebraMap_stalk_eq

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.GermToFunctionField_app_eq_of_fromSpecStalk_comp_eq
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicCurve
namespace GlueAux

Lean source · statement

theorem comp_algebraMap_stalk_eq
    {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y] (π : Y ⟶ X)
    (φ : X.functionField →+* Y.functionField)
    (hφπ : Y.fromSpecStalk (genericPoint Y) ≫ π =
      Spec.map (CommRingCat.ofHom φ) ≫ X.fromSpecStalk (genericPoint X))
    (y : Y) :
    φ.comp (algebraMap (X.presheaf.stalk (π y)) X.functionField) =
      (algebraMap (Y.presheaf.stalk y) Y.functionField).comp (π.stalkMap y).hom

theorem

germToFunctionField_app_eq_of_fromSpecStalk_comp_eq

L91 ↗

AlgebraicCurve.germToFunctionField_app_eq_of_fromSpecStalk_comp_eq

Source context 4 commands