NYLL
Module

Trace.lean

Nyll.AlgebraicCurves.Differentials.Trace
2 declarations indexed from sourceView source ↗

Module documentation

Trace

Imports2
  • Mathlib.RingTheory.Kaehler.Basic
  • Mathlib.RingTheory.Trace.Defs
Imported by6

Declarations

def

IsTraceDiff

L29 ↗
AlgebraicCurve.IsTraceDiff
Documentation

Compatibility of a differential trace map with the field trace on scalar multiples.

Source context 3 commands

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

noncomputable section
namespace AlgebraicCurve
variable (K F F' : Type*) [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
  [Algebra F F'] [IsScalarTower K F F']
Lean source · statement
def IsTraceDiff (t : Ω[F'⁄K] →ₗ[F] Ω[F⁄K]) : Prop
def

traceDiff

L35 ↗
AlgebraicCurve.traceDiff
Documentation

A differential trace map when one exists, and the zero map otherwise.

Source context 4 commands

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

noncomputable section
namespace AlgebraicCurve
variable (K F F' : Type*) [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
  [Algebra F F'] [IsScalarTower K F F']
open scoped Classical in
Lean source · statement
def traceDiff : Ω[F'⁄K] →ₗ[F] Ω[F⁄K]

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