NYLL
Module

TraceDiff_apply.lean

Nyll.AlgebraicCurves.Differentials.TraceDiff_apply
3 declarations indexed from sourceView source ↗

Module documentation

Trace Diff apply

Imports3
Imported by4

Declarations

theorem

exists_isTraceDiff

L33 ↗
AlgebraicCurves.Differentials.Proofs.TraceDiff_apply.AlgebraicCurve.exists_isTraceDiff
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.TraceDiff_apply
open _root_.AlgebraicCurve
open scoped AlgebraicCurve in
open TensorProduct in
Lean source · statement
theorem AlgebraicCurve.exists_isTraceDiff (K F F' : Type*) [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsSeparable F F'] : ∃
  t : Ω[F'⁄K] →ₗ[F] Ω[F⁄K], IsTraceDiff K F F' t
theorem

isTraceDiff_traceDiff

L47 ↗
AlgebraicCurves.Differentials.Proofs.TraceDiff_apply.AlgebraicCurve.isTraceDiff_traceDiff
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.TraceDiff_apply
open _root_.AlgebraicCurve
open scoped AlgebraicCurve in
Lean source · statement
theorem AlgebraicCurve.isTraceDiff_traceDiff (K F F' : Type*) [Field K] [Field F] [Field
  F'] [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsSeparable F F']
  : IsTraceDiff K F F' (traceDiff K F F')
theorem

traceDiff_apply

L54 ↗
AlgebraicCurve.traceDiff_apply
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.TraceDiff_apply
open _root_.AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.traceDiff_apply (K F F' : Type*) [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsSeparable F F'] (y
  : F') (ω : Ω[F⁄K]) : traceDiff K F F' (y • KaehlerDifferential.map K K F F' ω) = Algebra.trace F
  F' y • ω

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