Module

Differential_pullbackAlong_traceAlong_eq_traceAlong_pullbackAlong_of_algEquiv.lean

Nyll.AlgebraicCurves.Differentials.Differential_pullbackAlong_traceAlong_eq_traceAlong_pullbackAlong_of_algEquiv

4 declarations indexed from sourceView source ↗

Module documentation

Differential pullback Along trace Along eq trace Along pullback Along of alg Equiv

Imports2

Imported by1

Nyll.AlgebraicCurves.Differentials.All

theorem

pullbackAlong_square

L32 ↗

AlgebraicCurves.Differentials.Proofs.Differential_pullbackAlong_traceAlong_eq_traceAlong_pullbackAlong_of_algEquiv.TraceNatSol.pullbackAlong_square

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs
namespace Differential_pullbackAlong_traceAlong_eq_traceAlong_pullbackAlong_of_algEquiv
open AlgebraicCurve AlgebraicCurve.Differential KaehlerDifferential TensorProduct
namespace TraceNatSol
variable {K F F' F₀ F₀' : Type*} [Field K] [Field F] [Field F'] [Field F₀] [Field F₀']
  [Algebra K F] [Algebra K F'] [Algebra K F₀] [Algebra K F₀']

Lean source · statement

theorem pullbackAlong_square (φ' : F →ₐ[K] F') (φ : F₀ →ₐ[K] F₀') (θ : F →ₐ[K] F₀) (θ' : F' →ₐ[K]
  F₀')
    (hφ : ∀ x : F, θ' (φ' x) = φ (θ x)) (ω : Ω[F⁄K]) :
    pullbackAlong θ' (pullbackAlong φ' ω) = pullbackAlong φ (pullbackAlong θ ω)

theorem

separableAlong_of_algEquiv

L49 ↗

AlgebraicCurves.Differentials.Proofs.Differential_pullbackAlong_traceAlong_eq_traceAlong_pullbackAlong_of_algEquiv.TraceNatSol.separableAlong_of_algEquiv

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs
namespace Differential_pullbackAlong_traceAlong_eq_traceAlong_pullbackAlong_of_algEquiv
open AlgebraicCurve AlgebraicCurve.Differential KaehlerDifferential TensorProduct
namespace TraceNatSol
variable {K F F' F₀ F₀' : Type*} [Field K] [Field F] [Field F'] [Field F₀] [Field F₀']
  [Algebra K F] [Algebra K F'] [Algebra K F₀] [Algebra K F₀']

Lean source · statement

theorem separableAlong_of_algEquiv (φ' : F →ₐ[K] F') (φ : F₀ →ₐ[K] F₀') (θ : F ≃ₐ[K] F₀) (θ' : F'
  ≃ₐ[K] F₀')
    (hφ : ∀ x : F, θ' (φ' x) = φ (θ x)) (hsep : SeparableAlong K φ') : SeparableAlong K φ

theorem

trace_of_algEquiv

L59 ↗

AlgebraicCurves.Differentials.Proofs.Differential_pullbackAlong_traceAlong_eq_traceAlong_pullbackAlong_of_algEquiv.TraceNatSol.trace_of_algEquiv

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs
namespace Differential_pullbackAlong_traceAlong_eq_traceAlong_pullbackAlong_of_algEquiv
open AlgebraicCurve AlgebraicCurve.Differential KaehlerDifferential TensorProduct
namespace TraceNatSol
variable {K F F' F₀ F₀' : Type*} [Field K] [Field F] [Field F'] [Field F₀] [Field F₀']
  [Algebra K F] [Algebra K F'] [Algebra K F₀] [Algebra K F₀']

Lean source · full declaration

theorem trace_of_algEquiv (φ' : F →ₐ[K] F') (φ : F₀ →ₐ[K] F₀') (θ : F ≃ₐ[K] F₀) (θ' : F' ≃ₐ[K] F₀')
    (hφ : ∀ x : F, θ' (φ' x) = φ (θ x)) (u : F') :
    θ (letI := algebraAlong φ'; Algebra.trace F F' u) = (letI := algebraAlong φ; Algebra.trace F₀
      F₀' (θ' u)) := by
  let := algebraAlong φ'
  let := algebraAlong φ
  have h := Algebra.trace_eq_of_equiv_equiv θ.toRingEquiv θ'.toRingEquiv (by
    ext x
    exact (hφ x).symm) u
  rw [h]
  exact θ.toRingEquiv.apply_symm_apply _

theorem

pullbackAlong_traceAlong_eq_traceAlong_pullbackAlong_of_algEquiv

L84 ↗

AlgebraicCurve.Differential.pullbackAlong_traceAlong_eq_traceAlong_pullbackAlong_of_algEquiv

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurve.Differential
open _root_.AlgebraicCurves.Differentials.Proofs in
open Differential_pullbackAlong_traceAlong_eq_traceAlong_pullbackAlong_of_algEquiv in
open AlgebraicCurve AlgebraicCurve.Differential KaehlerDifferential TensorProduct in
open TraceNatSol in

Lean source · statement

theorem pullbackAlong_traceAlong_eq_traceAlong_pullbackAlong_of_algEquiv
    {K F F' F₀ F₀' : Type*} [Field K] [Field F] [Field F'] [Field F₀] [Field F₀']
    [Algebra K F] [Algebra K F'] [Algebra K F₀] [Algebra K F₀']
    (φ' : F →ₐ[K] F') (φ : F₀ →ₐ[K] F₀') (θ : F ≃ₐ[K] F₀) (θ' : F' ≃ₐ[K] F₀')
    (hφ : ∀ x : F, θ' (φ' x) = φ (θ x)) (hsep : AlgebraicCurve.SeparableAlong K φ') (η : Ω[F'⁄K]) :
    AlgebraicCurve.Differential.pullbackAlong (θ : F →ₐ[K] F₀)
      (AlgebraicCurve.Differential.traceAlong φ' η) =
      AlgebraicCurve.Differential.traceAlong φ (AlgebraicCurve.Differential.pullbackAlong (θ' : F'
        →ₐ[K] F₀') η)

Module documentation

Differential pullback Along trace Along eq trace Along pullback Along of alg Equiv

Declarations

pullbackAlong_square

separableAlong_of_algEquiv

trace_of_algEquiv

pullbackAlong_traceAlong_eq_traceAlong_pullbackAlong_of_algEquiv