NYLL
Module

FunctionFieldScalarFunctoriality.lean

Nyll.AlgebraicCurves.Models.FunctionFieldScalarFunctoriality
2 declarations indexed from sourceView source ↗

Module documentation

Scalar compatibility of actual function-field pullback

Imports2
Imported by4

Declarations

theorem

functionFieldMap_baseToFunctionField

L24 ↗
AlgebraicGeometry.Scheme.Hom.functionFieldMap_baseToFunctionField
Documentation

Actual function-field pullback commutes with the actual structure maps to the ground field.

Source context 5 commands

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

noncomputable section
open CategoryTheory TopologicalSpace AlgebraicCurve
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {K : Type u} [Field K] {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
Lean source · statement
theorem functionFieldMap_baseToFunctionField
    (c : X ⟶ Spec (.of K)) (f : Y ⟶ X) (hf : DenseRange f) (a : K) :
    f.functionFieldMap hf (baseToFunctionField c a) =
      baseToFunctionField (f ≫ c) a
def

functionFieldAlgHomOver

L43 ↗
AlgebraicGeometry.Scheme.Hom.functionFieldAlgHomOver
Documentation

The literal map of function fields as a homomorphism over the actual ground-field algebra structures.

Source context 5 commands

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

noncomputable section
open CategoryTheory TopologicalSpace AlgebraicCurve
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {K : Type u} [Field K] {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
Lean source · full declaration
def functionFieldAlgHomOver
    (c : X ⟶ Spec (.of K)) (f : Y ⟶ X) (hf : DenseRange f) :
    let : Algebra K X.functionField := (baseToFunctionField c).toAlgebra
    let : Algebra K Y.functionField := (baseToFunctionField (f ≫ c)).toAlgebra
    X.functionField →ₐ[K] Y.functionField := by
  let : Algebra K X.functionField := (baseToFunctionField c).toAlgebra
  let : Algebra K Y.functionField := (baseToFunctionField (f ≫ c)).toAlgebra
  exact
    { f.functionFieldMap hf with
      commutes' := functionFieldMap_baseToFunctionField c f hf }

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