Module

TraceDiff_inv_smul_D_eq_inv_norm_smul_D_norm.lean

Nyll.AlgebraicCurves.Differentials.TraceDiff_inv_smul_D_eq_inv_norm_smul_D_norm

7 declarations indexed from sourceView source ↗

Module documentation

Trace Diff inv smul D eq inv norm smul D norm

Imports12

Mathlib.RingTheory.Norm.Basic
Mathlib.RingTheory.Norm.Transitivity
Mathlib.RingTheory.Trace.Basic
Mathlib.RingTheory.Derivation.Basic
Mathlib.RingTheory.Derivation.MapCoeffs
Mathlib.FieldTheory.Separable
Mathlib.RingTheory.Etale.Kaehler
Mathlib.RingTheory.Etale.Field
Mathlib.LinearAlgebra.Dual.Lemmas
Nyll.AlgebraicCurves.Differentials.Trace
Nyll.AlgebraicCurves.Differentials.TraceDiff_apply
Nyll.AlgebraicCurves.Differentials.Kaehler.Algebra_trace_inv_mul_derivation_eq_inv_norm_mul_derivation_norm

Imported by2

theorem

O3a_local

L38 ↗

AlgebraicCurves.Differentials.Proofs.TraceDiff_inv_smul_D_eq_inv_norm_smul_D_norm.O3bAux1.O3a_local

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.TraceDiff_inv_smul_D_eq_inv_norm_smul_D_norm
open Module
namespace O3bAux1

Lean source · statement

theorem O3a_local {R F F' : Type*} [CommRing R] [Field F] [Field F'] [Algebra R F] [Algebra R F']
  [Algebra F F'] (d : Derivation R F F) (d' : Derivation R F' F') (hd : ∀ x : F, d' (algebraMap F
  F' x) = algebraMap F F' (d x)) (h : F') : Algebra.trace F F' (h⁻¹ * d' h) = (Algebra.norm F h)⁻¹
  * d (Algebra.norm F h)

theorem

isBaseChange

L49 ↗

AlgebraicCurves.Differentials.Proofs.TraceDiff_inv_smul_D_eq_inv_norm_smul_D_norm.O3bAux1.isBaseChange

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.TraceDiff_inv_smul_D_eq_inv_norm_smul_D_norm
open Module
namespace O3bAux1
section
variable (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']

Lean source · statement

theorem isBaseChange : IsBaseChange F' (KaehlerDifferential.map K K F F')

def

psi

L56 ↗

AlgebraicCurves.Differentials.Proofs.TraceDiff_inv_smul_D_eq_inv_norm_smul_D_norm.O3bAux1.psi

Documentation

The linear functional on extended differentials induced by base change.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.TraceDiff_inv_smul_D_eq_inv_norm_smul_D_norm
open Module
namespace O3bAux1
section
variable (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']
variable {K F F'}

Lean source · statement

def psi (φ : Ω[F⁄K] →ₗ[F] F) : Ω[F'⁄K] →ₗ[F'] F'

theorem

psi_map

L59 ↗

AlgebraicCurves.Differentials.Proofs.TraceDiff_inv_smul_D_eq_inv_norm_smul_D_norm.O3bAux1.psi_map

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.TraceDiff_inv_smul_D_eq_inv_norm_smul_D_norm
open Module
namespace O3bAux1
section
variable (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']
variable {K F F'}

Lean source · statement

theorem psi_map (φ : Ω[F⁄K] →ₗ[F] F) (ω : Ω[F⁄K]) :
    psi (F' := F') φ (KaehlerDifferential.map K K F F' ω) = algebraMap F F' (φ ω)

theorem

pair

L63 ↗

AlgebraicCurves.Differentials.Proofs.TraceDiff_inv_smul_D_eq_inv_norm_smul_D_norm.O3bAux1.pair

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.TraceDiff_inv_smul_D_eq_inv_norm_smul_D_norm
open Module
namespace O3bAux1
section
variable (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']
variable {K F F'}

Lean source · statement

theorem pair (φ : Ω[F⁄K] →ₗ[F] F) (n : Ω[F'⁄K]) :
    ∀ s : F', φ (AlgebraicCurve.traceDiff K F F' (s • n)) =
      Algebra.trace F F' (s * psi φ n)

theorem

main

L75 ↗

AlgebraicCurves.Differentials.Proofs.TraceDiff_inv_smul_D_eq_inv_norm_smul_D_norm.O3bAux1.main

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.TraceDiff_inv_smul_D_eq_inv_norm_smul_D_norm
open Module
namespace O3bAux1
section
variable (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']
variable {K F F'}

Lean source · statement

theorem main (h : F') :
    AlgebraicCurve.traceDiff K F F' (h⁻¹ • KaehlerDifferential.D K F' h) =
      (Algebra.norm F h)⁻¹ • KaehlerDifferential.D K F (Algebra.norm F h)

theorem

traceDiff_inv_smul_D_eq_inv_norm_smul_D_norm

L95 ↗

AlgebraicCurve.traceDiff_inv_smul_D_eq_inv_norm_smul_D_norm

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.TraceDiff_inv_smul_D_eq_inv_norm_smul_D_norm
open Module
open AlgebraicCurve in

Lean source · statement

theorem _root_.AlgebraicCurve.traceDiff_inv_smul_D_eq_inv_norm_smul_D_norm (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'] (h : F') : traceDiff K F F' (h⁻¹ • KaehlerDifferential.D K F' h) =
  (Algebra.norm F h)⁻¹ • KaehlerDifferential.D K F (Algebra.norm F h)

Module documentation

Trace Diff inv smul D eq inv norm smul D norm

Declarations

O3a_local

isBaseChange

psi

psi_map

pair

main

traceDiff_inv_smul_D_eq_inv_norm_smul_D_norm