Module

Differential_pullbackAlong_traceAlong_pullbackAlong_eq_traceAlong_pullbackAlong_pullbackAlong_of_swap.lean

Nyll.AlgebraicCurves.Differentials.Differential_pullbackAlong_traceAlong_pullbackAlong_eq_traceAlong_pullbackAlong_pullbackAlong_of_swap

4 declarations indexed from sourceView source ↗

Module documentation

Differential pullback Along trace Along pullback Along eq trace Along pullback Along

pullback Along of swap

Imports1

Nyll.AlgebraicCurves.Differentials.Maps

Imported by1

Nyll.AlgebraicCurves.Differentials.All

theorem

pullbackAlong_comp

L32 ↗

AlgebraicCurves.Differentials.Proofs.DifferentialTracePullbackSwap.E3WBody.pullbackAlong_comp

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.DifferentialTracePullbackSwap
open AlgebraicCurve KaehlerDifferential
open scoped TensorProduct
namespace E3WBody
variable {K F F' F'' : Type*} [Field K] [Field F] [Field F'] [Field F'']
  [Algebra K F] [Algebra K F'] [Algebra K F'']

Lean source · statement

theorem pullbackAlong_comp (f : F →ₐ[K] F') (g : F' →ₐ[K] F'') (ω : Ω[F⁄K]) :
    Differential.pullbackAlong (g.comp f) ω =
      Differential.pullbackAlong g (Differential.pullbackAlong f ω)

theorem

pullbackAlong_congr

L49 ↗

AlgebraicCurves.Differentials.Proofs.DifferentialTracePullbackSwap.E3WBody.pullbackAlong_congr

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.DifferentialTracePullbackSwap
open AlgebraicCurve KaehlerDifferential
open scoped TensorProduct
namespace E3WBody
variable {K F F' F'' : Type*} [Field K] [Field F] [Field F'] [Field F'']
  [Algebra K F] [Algebra K F'] [Algebra K F'']

Lean source · statement

theorem pullbackAlong_congr {f g : F →ₐ[K] F'} (h : ∀ x, f x = g x) :
    Differential.pullbackAlong f = Differential.pullbackAlong g

theorem

pullbackAlong_traceAlong_of_conj

L54 ↗

AlgebraicCurves.Differentials.Proofs.DifferentialTracePullbackSwap.E3WBody.pullbackAlong_traceAlong_of_conj

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.DifferentialTracePullbackSwap
open AlgebraicCurve KaehlerDifferential
open scoped TensorProduct
namespace E3WBody
variable {K F F' F'' : Type*} [Field K] [Field F] [Field F'] [Field F'']
  [Algebra K F] [Algebra K F'] [Algebra K F'']

Lean source · statement

theorem pullbackAlong_traceAlong_of_conj (φ φ' : F →ₐ[K] F') (hφ : SeparableAlong K φ)
    (hφ' : SeparableAlong K φ') (w : F ≃ₐ[K] F) (w' : F' ≃ₐ[K] F')
    (hconj : ∀ x : F, w' (φ x) = φ' (w x)) (η : Ω[F'⁄K]) :
    Differential.pullbackAlong (w : F →ₐ[K] F) (Differential.traceAlong φ η) =
      Differential.traceAlong φ' (Differential.pullbackAlong (w' : F' →ₐ[K] F') η)

theorem

pullbackAlong_traceAlong_pullbackAlong_eq_traceAlong_pullbackAlong_pullbackAlong_of_swap

L104 ↗

AlgebraicCurve.Differential.pullbackAlong_traceAlong_pullbackAlong_eq_traceAlong_pullbackAlong_pullbackAlong_of_swap

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurve.Differential
open _root_.AlgebraicCurves.Differentials.Proofs.DifferentialTracePullbackSwap
open _root_.AlgebraicCurve _root_.KaehlerDifferential
open scoped _root_.TensorProduct

Lean source · statement

theorem pullbackAlong_traceAlong_pullbackAlong_eq_traceAlong_pullbackAlong_pullbackAlong_of_swap
    {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
    (α β : F →ₐ[K] F') (hα : SeparableAlong K α) (hβ : SeparableAlong K β)
    (w : F ≃ₐ[K] F) (w' : F' ≃ₐ[K] F')
    (hswapα : ∀ x : F, w' (α x) = β (w x)) (hswapβ : ∀ x : F, w' (β x) = α (w x))
    (ω : Ω[F⁄K]) :
    Differential.pullbackAlong w.toAlgHom (Differential.traceAlong α (Differential.pullbackAlong β
      ω)) =
      Differential.traceAlong β (Differential.pullbackAlong α (Differential.pullbackAlong
        w.toAlgHom ω))

Module documentation

Differential pullback Along trace Along pullback Along eq trace Along pullback Along

Declarations

pullbackAlong_comp

pullbackAlong_congr

pullbackAlong_traceAlong_of_conj

pullbackAlong_traceAlong_pullbackAlong_eq_traceAlong_pullbackAlong_pullbackAlong_of_swap