NYLL
Module

CurveModel_ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified.lean

Nyll.AlgebraicCurves.Models.CurveModel_ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified
8 declarations indexed from sourceView source ↗

Module documentation

Curve Model ramification Index Along point Equiv Place eq one of formally Unramified

Imports6
Imported by4

Declarations

theorem

apply_genericPoint_eq

L42 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified.E1bSol.apply_genericPoint_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
open Topology
noncomputable section
namespace E1bSol
section FieldMap
variable {X Y Z : Scheme.{u}} [IsIntegral X] [IsIntegral Y] [IsIntegral Z]
Lean source · statement
theorem apply_genericPoint_eq (f : X ⟶ Y) [Flat f] : f.base (genericPoint X) = genericPoint Y
def

fieldMap

L53 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified.E1bSol.fieldMap
Documentation

The homomorphism of function fields induced by a morphism preserving the generic point.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
open Topology
noncomputable section
namespace E1bSol
section FieldMap
variable {X Y Z : Scheme.{u}} [IsIntegral X] [IsIntegral Y] [IsIntegral Z]
Lean source · statement
def fieldMap (f : X ⟶ Y) (h : f.base (genericPoint X) = genericPoint Y) :
    Y.functionField →+* X.functionField
theorem

fieldMap_eq

L59 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified.E1bSol.fieldMap_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
open Topology
noncomputable section
namespace E1bSol
section FieldMap
variable {X Y Z : Scheme.{u}} [IsIntegral X] [IsIntegral Y] [IsIntegral Z]
Lean source · statement
theorem fieldMap_eq (f : X ⟶ Y) (h : f.base (genericPoint X) = genericPoint Y) :
    CommRingCat.ofHom (fieldMap f h) =
      Y.presheaf.stalkSpecializes (specializes_of_eq h : f.base (genericPoint X) ⤳ genericPoint Y) ≫
        f.stalkMap (genericPoint X)
theorem

algebraMap_stalkMap

L64 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified.E1bSol.algebraMap_stalkMap
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
open Topology
noncomputable section
namespace E1bSol
section FieldMap
variable {X Y Z : Scheme.{u}} [IsIntegral X] [IsIntegral Y] [IsIntegral Z]
Lean source · statement
theorem algebraMap_stalkMap (f : X ⟶ Y) (h : f.base (genericPoint X) = genericPoint Y)
    (p : X) (s : Y.presheaf.stalk (f.base p)) :
    algebraMap _ X.functionField (f.stalkMap p s) = fieldMap f h (algebraMap _ Y.functionField s)
theorem

fieldMap_germToFunctionField

L76 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified.E1bSol.fieldMap_germToFunctionField
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
open Topology
noncomputable section
namespace E1bSol
section FieldMap
variable {X Y Z : Scheme.{u}} [IsIntegral X] [IsIntegral Y] [IsIntegral Z]
Lean source · statement
theorem fieldMap_germToFunctionField (f : X ⟶ Y) (h : f.base (genericPoint X) = genericPoint Y)
    (U : Y.Opens) [hU : Nonempty (U : Scheme.{u})] [hU' : Nonempty ((f ⁻¹ᵁ U : X.Opens) :
      Scheme.{u})]
    (s : Γ(Y, U)) :
    fieldMap f h (Y.germToFunctionField U s) = X.germToFunctionField (f ⁻¹ᵁ U) (f.app U s)
theorem

fieldMap_comp

L91 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified.E1bSol.fieldMap_comp
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
open Topology
noncomputable section
namespace E1bSol
section FieldMap
variable {X Y Z : Scheme.{u}} [IsIntegral X] [IsIntegral Y] [IsIntegral Z]
Lean source · statement
theorem fieldMap_comp (f : X ⟶ Y) (g : Y ⟶ Z) (hf : f.base (genericPoint X) = genericPoint Y)
    (hg : g.base (genericPoint Y) = genericPoint Z) (hfg : (f ≫ g).base (genericPoint X) =
      genericPoint Z) :
    fieldMap (f ≫ g) hfg = (fieldMap f hf).comp (fieldMap g hg)
theorem

fieldMap_eq_of_fromSpecStalk_comp_eq

L114 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified.E1bSol.fieldMap_eq_of_fromSpecStalk_comp_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
open Topology
noncomputable section
namespace E1bSol
section FieldMap
variable {X Y Z : Scheme.{u}} [IsIntegral X] [IsIntegral Y] [IsIntegral Z]
Lean source · statement
theorem fieldMap_eq_of_fromSpecStalk_comp_eq (f : X ⟶ Y) (h : f.base (genericPoint X) =
  genericPoint Y)
    (c : Y.functionField →+* X.functionField)
    (hc : X.fromSpecStalk (genericPoint X) ≫ f = Spec.map (CommRingCat.ofHom c) ≫ Y.fromSpecStalk
      (genericPoint Y)) :
    fieldMap f h = c
theorem

ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified

L150 ↗
AlgebraicCurve.CurveModel.ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurve
noncomputable section
universe u
open _root_.CategoryTheory _root_.CategoryTheory.Limits _root_.AlgebraicGeometry
open _root_.AlgebraicCurve _root_.Topology
open _root_.AlgebraicCurves.Models.Proofs in
open CurveModel_ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified in
open E1bSol in
Lean source · statement
theorem CurveModel.ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified
    {K : Type u} [Field K] [IsAlgClosed K]
    {L : Type u} [Field L] [Algebra K L] {L' : Type u} [Field L'] [Algebra K L']
    (M : CurveModel K L) (M' : CurveModel K L')
    (φ : L' →ₐ[K] L) (hφ : φ.toRingHom.IsIntegral)
    (πM : M.C ⟶ M'.C) (hπM : πM ≫ M'.toBase = M.toBase)
    (hgen : M.C.fromSpecStalk (genericPoint M.C) ≫ πM =
      Spec.map (CommRingCat.ofHom (M.ffEquiv.toRingHom.comp (φ.toRingHom.comp
        M'.ffEquiv.symm.toRingHom))) ≫
        M'.C.fromSpecStalk (genericPoint M'.C))
    (y : {q : Spec (CommRingCat.of K) ⟶ M.C // q ≫ M.toBase = 𝟙 _})
    (V : M.C.Opens) (hyV : y.1.base (IsLocalRing.closedPoint K) ∈ V)
    (hV : FormallyUnramified (V.ι ≫ πM)) :
    Place.ramificationIndexAlong φ (M.pointEquivPlace y) = 1

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