NYLL
Module

Differential_pullbackAlong_traceAlong_eq_sum_lifts.lean

Nyll.AlgebraicCurves.Differentials.Differential_pullbackAlong_traceAlong_eq_sum_lifts
7 declarations indexed from sourceView source ↗

Module documentation

Differential pullback Along trace Along eq sum lifts

Imports2
Imported by1

Declarations

theorem

pullbackAlong_pullbackAlong

L37 ↗
AlgebraicCurves.Differentials.Proofs.Differential_pullbackAlong_traceAlong_eq_sum_lifts.AlgebraicCurve.TraceAtPoints.pullbackAlong_pullbackAlong
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_pullbackAlong_traceAlong_eq_sum_lifts
noncomputable section
open KaehlerDifferential TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceAtPoints
variable {K F F' E : Type*} [Field K] [Field F] [Field F'] [Field E]
  [Algebra K F] [Algebra K F'] [Algebra K E]
Lean source · statement
theorem pullbackAlong_pullbackAlong (ψ : F →ₐ[K] F') (σ : F' →ₐ[K] E) (ω : Ω[F⁄K]) :
    Differential.pullbackAlong σ (Differential.pullbackAlong ψ ω) =
      Differential.pullbackAlong (σ.comp ψ) ω
def

liftsAlong

L54 ↗
AlgebraicCurves.Differentials.Proofs.Differential_pullbackAlong_traceAlong_eq_sum_lifts.AlgebraicCurve.TraceAtPoints.liftsAlong
Documentation

The extensions of the given algebra embedding across the specified field homomorphism.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_pullbackAlong_traceAlong_eq_sum_lifts
noncomputable section
open KaehlerDifferential TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceAtPoints
variable {K F F' E : Type*} [Field K] [Field F] [Field F'] [Field E]
  [Algebra K F] [Algebra K F'] [Algebra K E]
Lean source · statement
def liftsAlong (φ : F →ₐ[K] F') (e : F →ₐ[K] E) : Set (F' →ₐ[K] E)
theorem

mem_liftsAlong

L56 ↗
AlgebraicCurves.Differentials.Proofs.Differential_pullbackAlong_traceAlong_eq_sum_lifts.AlgebraicCurve.TraceAtPoints.mem_liftsAlong
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_pullbackAlong_traceAlong_eq_sum_lifts
noncomputable section
open KaehlerDifferential TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceAtPoints
variable {K F F' E : Type*} [Field K] [Field F] [Field F'] [Field E]
  [Algebra K F] [Algebra K F'] [Algebra K E]
Lean source · statement
theorem mem_liftsAlong (φ : F →ₐ[K] F') (e : F →ₐ[K] E) (σ : F' →ₐ[K] E) :
    σ ∈ liftsAlong φ e ↔ σ.comp φ = e
theorem

liftsAlong_eq_range

L59 ↗
AlgebraicCurves.Differentials.Proofs.Differential_pullbackAlong_traceAlong_eq_sum_lifts.AlgebraicCurve.TraceAtPoints.liftsAlong_eq_range
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_pullbackAlong_traceAlong_eq_sum_lifts
noncomputable section
open KaehlerDifferential TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceAtPoints
variable {K F F' E : Type*} [Field K] [Field F] [Field F'] [Field E]
  [Algebra K F] [Algebra K F'] [Algebra K E]
Lean source · full declaration
theorem liftsAlong_eq_range (φ : F →ₐ[K] F') (e : F →ₐ[K] E)
    [Algebra F F'] [IsScalarTower K F F'] [Algebra F E] [IsScalarTower K F E]
    (hφ : ∀ x, algebraMap F F' x = φ x) (he : ∀ x, algebraMap F E x = e x) :
    liftsAlong φ e = Set.range (fun τ : F' →ₐ[F] E => τ.restrictScalars K) := by
  ext σ
  constructor
  · intro hσ
    refine ⟨{ σ.toRingHom with commutes' := fun x => ?_ }, ?_⟩
    · simp only [RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe,
        MonoidHom.coe_ofClass, hφ, he]
      exact congrArg (fun g : F →ₐ[K] E => g x) hσ
    · ext x; rfl
  · rintro ⟨τ, rfl⟩
    change (τ.restrictScalars K).comp φ = e
    ext x
    simp only [AlgHom.coe_comp, AlgHom.coe_restrictScalars', Function.comp_apply]
    rw [← hφ, τ.commutes, he]
theorem

sum_eq_sum_algHom

L77 ↗
AlgebraicCurves.Differentials.Proofs.Differential_pullbackAlong_traceAlong_eq_sum_lifts.AlgebraicCurve.TraceAtPoints.sum_eq_sum_algHom
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_pullbackAlong_traceAlong_eq_sum_lifts
noncomputable section
open KaehlerDifferential TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceAtPoints
variable {K F F' E : Type*} [Field K] [Field F] [Field F'] [Field E]
  [Algebra K F] [Algebra K F'] [Algebra K E]
Lean source · statement
theorem sum_eq_sum_algHom (φ : F →ₐ[K] F') (e : F →ₐ[K] E)
    (S : Finset (F' →ₐ[K] E)) (hS : ∀ σ : F' →ₐ[K] E, σ ∈ S ↔ σ.comp φ = e)
    [Algebra F F'] [IsScalarTower K F F'] [Algebra F E] [IsScalarTower K F E]
    (hφ : ∀ x, algebraMap F F' x = φ x) (he : ∀ x, algebraMap F E x = e x)
    [Fintype (F' →ₐ[F] E)] {M : Type*} [AddCommMonoid M] (g : (F' →ₐ[K] E) → M) :
    ∑ σ ∈ S, g σ = ∑ τ : F' →ₐ[F] E, g (τ.restrictScalars K)
theorem

pullbackAlong_traceAlong_eq_sum

L92 ↗
AlgebraicCurves.Differentials.Proofs.Differential_pullbackAlong_traceAlong_eq_sum_lifts.AlgebraicCurve.TraceAtPoints.pullbackAlong_traceAlong_eq_sum
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_pullbackAlong_traceAlong_eq_sum_lifts
noncomputable section
open KaehlerDifferential TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceAtPoints
variable {K F F' E : Type*} [Field K] [Field F] [Field F'] [Field E]
  [Algebra K F] [Algebra K F'] [Algebra K E]
Lean source · statement
theorem pullbackAlong_traceAlong_eq_sum [IsAlgClosed E] (φ : F →ₐ[K] F')
    (hfin : FiniteAlong K φ) (hsep : SeparableAlong K φ) (e : F →ₐ[K] E)
    (S : Finset (F' →ₐ[K] E)) (hS : ∀ σ : F' →ₐ[K] E, σ ∈ S ↔ σ.comp φ = e)
    (ω' : Ω[F'⁄K]) :
    Differential.pullbackAlong e (Differential.traceAlong φ ω') =
      ∑ σ ∈ S, Differential.pullbackAlong σ ω'
theorem

pullbackAlong_traceAlong_eq_sum_lifts

L134 ↗
AlgebraicCurve.Differential.pullbackAlong_traceAlong_eq_sum_lifts
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_pullbackAlong_traceAlong_eq_sum_lifts
open _root_.AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.Differential.pullbackAlong_traceAlong_eq_sum_lifts
    (K F F' E : Type*) [Field K] [Field F] [Field F'] [Field E]
    [Algebra K F] [Algebra K F'] [Algebra K E] [IsAlgClosed E]
    (φ : F →ₐ[K] F') (hfin : FiniteAlong K φ) (hsep : SeparableAlong K φ)
    (e : F →ₐ[K] E) (S : Finset (F' →ₐ[K] E)) (hS : ∀ σ : F' →ₐ[K] E, σ ∈ S ↔ σ.comp φ = e)
    (ω' : Ω[F'⁄K]) :
    Differential.pullbackAlong e (Differential.traceAlong φ ω') =
      ∑ σ ∈ S, Differential.pullbackAlong σ ω'

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