NYLL
Module

IsTraceDiff_traceDiff.lean

Nyll.AlgebraicCurves.Differentials.IsTraceDiff_traceDiff
6 declarations indexed from sourceView source ↗

Module documentation

Is Trace Diff trace Diff

Imports3
Imported by1

Declarations

theorem

exists_isTraceDiff

L32 ↗
AlgebraicCurves.Differentials.Proofs.IsTraceDiff_traceDiff.AlgebraicCurve.exists_isTraceDiff
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.IsTraceDiff_traceDiff
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_aux

L46 ↗
AlgebraicCurves.Differentials.Proofs.IsTraceDiff_traceDiff.AlgebraicCurve.isTraceDiff_traceDiff_aux
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.IsTraceDiff_traceDiff
open _root_.AlgebraicCurve
open scoped AlgebraicCurve in
Lean source · statement
theorem AlgebraicCurve.isTraceDiff_traceDiff_aux (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 ↗
AlgebraicCurves.Differentials.Proofs.IsTraceDiff_traceDiff.AlgebraicCurve.traceDiff_apply
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.IsTraceDiff_traceDiff
open _root_.AlgebraicCurve
open scoped AlgebraicCurve in
Lean source · statement
theorem 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 • ω
theorem

isTraceDiff_unique

L61 ↗
AlgebraicCurves.Differentials.Proofs.IsTraceDiff_traceDiff.AlgebraicCurve.isTraceDiff_unique
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.IsTraceDiff_traceDiff
open _root_.AlgebraicCurve
open scoped AlgebraicCurve in
Lean source · statement
theorem AlgebraicCurve.isTraceDiff_unique (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₁
  t₂ : Ω[F'⁄K] →ₗ[F] Ω[F⁄K]} (h₁ : IsTraceDiff K F F' t₁) (h₂ : IsTraceDiff K F F' t₂) : t₁ = t₂
theorem

eq_traceDiff_of_isTraceDiff

L76 ↗
AlgebraicCurves.Differentials.Proofs.IsTraceDiff_traceDiff.AlgebraicCurve.eq_traceDiff_of_isTraceDiff
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.IsTraceDiff_traceDiff
open _root_.AlgebraicCurve
open scoped AlgebraicCurve in
Lean source · statement
theorem AlgebraicCurve.eq_traceDiff_of_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]} (ht : IsTraceDiff K F F' t) : t = traceDiff
  K F F'
theorem

isTraceDiff_traceDiff

L82 ↗
AlgebraicCurve.isTraceDiff_traceDiff
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.IsTraceDiff_traceDiff
open _root_.AlgebraicCurve
Lean source · statement
theorem _root_.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')

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