Module

FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates.lean

Nyll.AlgebraicCurves.Differentials.Residues.FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates

18 declarations indexed from sourceView source ↗

Module documentation

Differentials, residues, and divisor correspondences

Separable extensions with generating coordinate differentials satisfy the fibre residue identity.

Imports8

Imported by3

def

FiberKaehlerCotraceResidueIdentity

L45 ↗

AlgebraicCurves.Differentials.Residues.Proofs.FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates.AlgebraicCurve.FiberKaehlerCotraceResidueIdentity

Documentation

The residue sum of a pulled-back differential over a place fibre agrees with the base differential residue of the field trace.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates
noncomputable section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.KaehlerDifferential
open _root_.ModularCurve.KwF4R1V391a
namespace AlgebraicCurve

Lean source · statement

def FiberKaehlerCotraceResidueIdentity
    (K F E : Type*) [Field K] [Field F] [Algebra K F]
    [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
    [HasCanonicalLocalResidueKStar K E] [HasCanonicalLocalResidueKStar K F]
    [Algebra.IsIntegral E F] : Prop

theorem

localResidueCompletion_spec

L62 ↗

AlgebraicCurves.Differentials.Residues.Proofs.FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates.AlgebraicCurve.localResidueCompletion_spec

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates
noncomputable section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.KaehlerDifferential
open _root_.ModularCurve.KwF4R1V391a
namespace AlgebraicCurve
variable {K F E : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [Field E] [Algebra K E] [HasCanonicalLocalResidueKStar K E]
variable [Algebra E F] [IsScalarTower K E F] [Algebra.IsIntegral E F]

Lean source · statement

theorem localResidueCompletion_spec (v : Place K E) (xh : v.adicCompletion)
    {x : E} (hx : algebraMap E v.adicCompletion x - xh ∈ v.adicCompletionIntegers) :
    kwHgfV352_localResidueCompletion v xh = v.localResidue x

theorem

localResidueCompletion_algebraMap

L82 ↗

AlgebraicCurves.Differentials.Residues.Proofs.FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates.AlgebraicCurve.localResidueCompletion_algebraMap

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates
noncomputable section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.KaehlerDifferential
open _root_.ModularCurve.KwF4R1V391a
namespace AlgebraicCurve
variable {K F E : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [Field E] [Algebra K E] [HasCanonicalLocalResidueKStar K E]
variable [Algebra E F] [IsScalarTower K E F] [Algebra.IsIntegral E F]

Lean source · statement

theorem localResidueCompletion_algebraMap (v : Place K E) (x : E) :
    kwHgfV352_localResidueCompletion v (algebraMap E v.adicCompletion x) =
      v.localResidue x

theorem

localResidueCompletion_add

L87 ↗

AlgebraicCurves.Differentials.Residues.Proofs.FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates.AlgebraicCurve.localResidueCompletion_add

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates
noncomputable section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.KaehlerDifferential
open _root_.ModularCurve.KwF4R1V391a
namespace AlgebraicCurve
variable {K F E : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [Field E] [Algebra K E] [HasCanonicalLocalResidueKStar K E]
variable [Algebra E F] [IsScalarTower K E F] [Algebra.IsIntegral E F]

Lean source · statement

theorem localResidueCompletion_add (v : Place K E) (xh yh : v.adicCompletion) :
    kwHgfV352_localResidueCompletion v (xh + yh) =
      kwHgfV352_localResidueCompletion v xh + kwHgfV352_localResidueCompletion v yh

theorem

localResidueCompletion_sum

L102 ↗

AlgebraicCurves.Differentials.Residues.Proofs.FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates.AlgebraicCurve.localResidueCompletion_sum

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates
noncomputable section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.KaehlerDifferential
open _root_.ModularCurve.KwF4R1V391a
namespace AlgebraicCurve
variable {K F E : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [Field E] [Algebra K E] [HasCanonicalLocalResidueKStar K E]
variable [Algebra E F] [IsScalarTower K E F] [Algebra.IsIntegral E F]

Lean source · statement

theorem localResidueCompletion_sum (v : Place K E) {ι : Type*}
    (s : Finset ι) (f : ι → v.adicCompletion) :
    kwHgfV352_localResidueCompletion v (∑ i ∈ s, f i) =
      ∑ i ∈ s, kwHgfV352_localResidueCompletion v (f i)

theorem

kaehlerPullback_smul

L117 ↗

AlgebraicCurves.Differentials.Residues.Proofs.FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates.AlgebraicCurve.kaehlerPullback_smul

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates
noncomputable section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.KaehlerDifferential
open _root_.ModularCurve.KwF4R1V391a
namespace AlgebraicCurve
variable {K F E : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [Field E] [Algebra K E] [HasCanonicalLocalResidueKStar K E]
variable [Algebra E F] [IsScalarTower K E F] [Algebra.IsIntegral E F]
omit [HasCanonicalLocalResidueKStar K F] [HasCanonicalLocalResidueKStar K E]
    [Algebra.IsIntegral E F] in

Lean source · statement

theorem kaehlerPullback_smul (g : E) (ωE : Ω[E⁄K]) :
    kaehlerPullback K F E (g • ωE) =
      algebraMap E F g • kaehlerPullback K F E ωE

theorem

completionTraceF_apply

L125 ↗

AlgebraicCurves.Differentials.Residues.Proofs.FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates.AlgebraicCurve.completionTraceF_apply

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates
noncomputable section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.KaehlerDifferential
open _root_.ModularCurve.KwF4R1V391a
namespace AlgebraicCurve
variable {K F E : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [Field E] [Algebra K E] [HasCanonicalLocalResidueKStar K E]
variable [Algebra E F] [IsScalarTower K E F] [Algebra.IsIntegral E F]
omit [HasCanonicalLocalResidueKStar K F] [HasCanonicalLocalResidueKStar K E] in

Lean source · statement

theorem completionTraceF_apply [FiniteDimensional E F] (w : Place K F) (g : F) :
    kw_ffgc_completionTraceF' E w g =
      Algebra.trace (w.restrict E).adicCompletion w.adicCompletion
        (algebraMap F w.adicCompletion g)

theorem

completionTraceF_mul_algebraMap

L131 ↗

AlgebraicCurves.Differentials.Residues.Proofs.FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates.AlgebraicCurve.completionTraceF_mul_algebraMap

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates
noncomputable section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.KaehlerDifferential
open _root_.ModularCurve.KwF4R1V391a
namespace AlgebraicCurve
variable {K F E : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [Field E] [Algebra K E] [HasCanonicalLocalResidueKStar K E]
variable [Algebra E F] [IsScalarTower K E F] [Algebra.IsIntegral E F]
omit [HasCanonicalLocalResidueKStar K F] [HasCanonicalLocalResidueKStar K E] in

Lean source · statement

theorem completionTraceF_mul_algebraMap [FiniteDimensional E F]
    (w : Place K F) (g : F) (c : E) :
    kw_ffgc_completionTraceF' E w (g * algebraMap E F c) =
      kw_ffgc_completionTraceF' E w g *
        algebraMap E (w.restrict E).adicCompletion c

theorem

completionTraceAt_mul_algebraMap

L142 ↗

AlgebraicCurves.Differentials.Residues.Proofs.FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates.AlgebraicCurve.completionTraceAt_mul_algebraMap

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates
noncomputable section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.KaehlerDifferential
open _root_.ModularCurve.KwF4R1V391a
namespace AlgebraicCurve
variable {K F E : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [Field E] [Algebra K E] [HasCanonicalLocalResidueKStar K E]
variable [Algebra E F] [IsScalarTower K E F] [Algebra.IsIntegral E F]
omit [HasCanonicalLocalResidueKStar K F] [HasCanonicalLocalResidueKStar K E] in

Lean source · statement

theorem completionTraceAt_mul_algebraMap [FiniteDimensional E F]
    [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
    (v : Place K E) (w : Place K F) (hw : w ∈ v.fiber F) (g : F) (c : E) :
    kwHgfV352_completionTraceAt v w hw (g * algebraMap E F c) =
      kwHgfV352_completionTraceAt v w hw g *
        algebraMap E v.adicCompletion c

theorem

kaehlerResidueTerm_pullback_diagonal_eq_dCoord_shift

L157 ↗

AlgebraicCurves.Differentials.Residues.Proofs.FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates.AlgebraicCurve.kaehlerResidueTerm_pullback_diagonal_eq_dCoord_shift

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates
noncomputable section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.KaehlerDifferential
open _root_.ModularCurve.KwF4R1V391a
namespace AlgebraicCurve
variable {K F E : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [Field E] [Algebra K E] [HasCanonicalLocalResidueKStar K E]
variable [Algebra E F] [IsScalarTower K E F] [Algebra.IsIntegral E F]
omit [HasCanonicalLocalResidueKStar K E] [Algebra.IsIntegral E F] in

Lean source · statement

theorem kaehlerResidueTerm_pullback_diagonal_eq_dCoord_shift
    [Nontrivial Ω[F⁄K]] [Nontrivial Ω[E⁄K]]
    (v : Place K E) [v.DCoordGenerates]
    (w : Place K F) [w.DCoordGenerates] (ωE : Ω[E⁄K]) (g : F) :
    kaehlerResidueTerm (kaehlerPullback K F E ωE) (diagonalHom K F g) w =
      kaehlerResidueTerm (kaehlerPullback K F E v.dCoord)
        (diagonalHom K F (g * algebraMap E F (v.differentialCoeff ωE))) w

theorem

fiberKaehlerCotraceResidueIdentity_of_rtcc_cts

L174 ↗

AlgebraicCurves.Differentials.Residues.Proofs.FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates.AlgebraicCurve.fiberKaehlerCotraceResidueIdentity_of_rtcc_cts

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates
noncomputable section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.KaehlerDifferential
open _root_.ModularCurve.KwF4R1V391a
namespace AlgebraicCurve
variable {K F E : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [Field E] [Algebra K E] [HasCanonicalLocalResidueKStar K E]
variable [Algebra E F] [IsScalarTower K E F] [Algebra.IsIntegral E F]

Lean source · statement

theorem fiberKaehlerCotraceResidueIdentity_of_rtcc_cts
    [∀ w : Place K F, w.FiniteResidue] [FiniteDimensional E F]
    [Nontrivial Ω[E⁄K]] [∀ v : Place K E, v.DCoordGenerates]
    [Nontrivial Ω[F⁄K]] [∀ w : Place K F, w.DCoordGenerates]
    (hRTCC : ∀ [HasPrincipalDivisors K E] [HasPrincipalDivisors K F],
      KwF4R1V391aResidueTraceCompletionCommute K F E)
    (hCTS : KwHgfV352CompletionTraceSum K F E) :
    FiberKaehlerCotraceResidueIdentity K F E

theorem

kaehlerResidueTerm_smul_diagonal

L216 ↗

AlgebraicCurves.Differentials.Residues.Proofs.FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates.AlgebraicCurve.kaehlerResidueTerm_smul_diagonal

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates
noncomputable section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.KaehlerDifferential
open _root_.ModularCurve.KwF4R1V391a
namespace AlgebraicCurve
variable {K F E : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [Field E] [Algebra K E] [HasCanonicalLocalResidueKStar K E]
variable [Algebra E F] [IsScalarTower K E F] [Algebra.IsIntegral E F]

Lean source · statement

theorem kaehlerResidueTerm_smul_diagonal
    [Nontrivial Ω[F⁄K]] (g : F) (ω : Ω[F⁄K]) (f : F)
    (v : Place K F) [v.DCoordGenerates] :
    kaehlerResidueTerm (g • ω) (diagonalHom K F f) v =
      kaehlerResidueTerm ω (diagonalHom K F (g * f)) v

theorem

finsum_place_eq_finsum_fiber_sum

L227 ↗

AlgebraicCurves.Differentials.Residues.Proofs.FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates.AlgebraicCurve.finsum_place_eq_finsum_fiber_sum

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates
noncomputable section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.KaehlerDifferential
open _root_.ModularCurve.KwF4R1V391a
namespace AlgebraicCurve
variable {K F E : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [Field E] [Algebra K E] [HasCanonicalLocalResidueKStar K E]
variable [Algebra E F] [IsScalarTower K E F] [Algebra.IsIntegral E F]
omit [HasCanonicalLocalResidueKStar K F] [HasCanonicalLocalResidueKStar K E] in

Lean source · statement

theorem finsum_place_eq_finsum_fiber_sum
    {M : Type*} [AddCommMonoid M] [HasPrincipalDivisors K F]
    (g : Place K F → M) (hg : (Function.support g).Finite) :
    ∑ᶠ w, g w = ∑ᶠ v : Place K E, ∑ w ∈ v.fiber F, g w

theorem

residueTheorem_of_fiberKaehlerCotraceResidueIdentity

L258 ↗

AlgebraicCurves.Differentials.Residues.Proofs.FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates.AlgebraicCurve.residueTheorem_of_fiberKaehlerCotraceResidueIdentity

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates
noncomputable section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.KaehlerDifferential
open _root_.ModularCurve.KwF4R1V391a
namespace AlgebraicCurve
variable {K F E : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [Field E] [Algebra K E] [HasCanonicalLocalResidueKStar K E]
variable [Algebra E F] [IsScalarTower K E F] [Algebra.IsIntegral E F]

Lean source · statement

theorem residueTheorem_of_fiberKaehlerCotraceResidueIdentity
    [HasCanonicalDivisor (K := K) (F := F)]
    [∀ w : Place K F, w.DCoordGenerates] [Nontrivial Ω[F⁄K]]
    [HasCanonicalDivisor (K := K) (F := E)]
    [∀ v : Place K E, v.DCoordGenerates] [Nontrivial Ω[E⁄K]]
    [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
    (hE : ResidueTheorem K E) {ωE₀ : Ω[E⁄K]} (hωE₀ : ωE₀ ≠ 0)
    (hgen : kaehlerPullback K F E ωE₀ ≠ 0)
    (hIdent : FiberKaehlerCotraceResidueIdentity K F E) :
    ResidueTheorem K F

theorem

mapBaseChange_surjective_of_subsingleton

L320 ↗

AlgebraicCurves.Differentials.Residues.Proofs.FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates.AlgebraicCurve.mapBaseChange_surjective_of_subsingleton

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates
noncomputable section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.KaehlerDifferential
open _root_.ModularCurve.KwF4R1V391a
namespace AlgebraicCurve
variable {K F E : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [Field E] [Algebra K E] [HasCanonicalLocalResidueKStar K E]
variable [Algebra E F] [IsScalarTower K E F] [Algebra.IsIntegral E F]
omit [HasCanonicalLocalResidueKStar K F] [HasCanonicalLocalResidueKStar K E]
    [Algebra.IsIntegral E F] in

Lean source · statement

theorem mapBaseChange_surjective_of_subsingleton [Subsingleton Ω[F⁄E]] :
    Function.Surjective (KaehlerDifferential.mapBaseChange K E F)

theorem

exists_kaehlerPullback_ne_zero

L328 ↗

AlgebraicCurves.Differentials.Residues.Proofs.FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates.AlgebraicCurve.exists_kaehlerPullback_ne_zero

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates
noncomputable section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.KaehlerDifferential
open _root_.ModularCurve.KwF4R1V391a
namespace AlgebraicCurve
variable {K F E : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [Field E] [Algebra K E] [HasCanonicalLocalResidueKStar K E]
variable [Algebra E F] [IsScalarTower K E F] [Algebra.IsIntegral E F]
omit [HasCanonicalLocalResidueKStar K F] [HasCanonicalLocalResidueKStar K E]
    [Algebra.IsIntegral E F] in

Lean source · statement

theorem exists_kaehlerPullback_ne_zero
    [Algebra.IsSeparable E F] [Nontrivial Ω[F⁄K]] :
    ∃ ωE : Ω[E⁄K], kaehlerPullback K F E ωE ≠ 0

theorem

kaehlerPullback_ne_zero

L351 ↗

AlgebraicCurves.Differentials.Residues.Proofs.FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates.AlgebraicCurve.kaehlerPullback_ne_zero

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates
noncomputable section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.KaehlerDifferential
open _root_.ModularCurve.KwF4R1V391a
namespace AlgebraicCurve
variable {K F E : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [Field E] [Algebra K E] [HasCanonicalLocalResidueKStar K E]
variable [Algebra E F] [IsScalarTower K E F] [Algebra.IsIntegral E F]
omit [HasCanonicalLocalResidueKStar K F] [HasCanonicalLocalResidueKStar K E]
    [Algebra.IsIntegral E F] in

Lean source · statement

theorem kaehlerPullback_ne_zero
    [Algebra.IsSeparable E F] [Nontrivial Ω[F⁄K]] [Nontrivial Ω[E⁄K]]
    (v : Place K E) [v.DCoordGenerates] {ωE : Ω[E⁄K]} (hωE : ωE ≠ 0) :
    kaehlerPullback K F E ωE ≠ 0

theorem