TwoChartCech.Cover.LaurentChart.residue_eq_kaehlerResidueTerm
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.Cover_LaurentChart_residue_eq_kaehlerResidueTerm
attribute [-instance]
AlgebraicCurve.instHasCanonicalLocalResidueK
AlgebraicCurve.Place.instAlgebra_restrictResidueField
AlgebraicCurve.Place.instIsScalarTower_restrictResidueField
AlgebraicCurve.instHasLocalResidue
AlgebraicCurve.HasSeparableResidue.of_perfectField_of_isCurveOver
AlgebraicCurve.HasSeparableResidue.of_perfectField
AlgebraicCurve.Place.instIsLocalHom_restrictSubringHom
AlgebraicCurve.instHasCanonicalLocalResidueKStar
ModularCurve.KwNo6Pin.isLocalRing_completion
AlgebraicCurve.IsCurveOver.instNontrivialKaehler
AlgebraicCurve.IsCurveOver.instFreeKaehler
AlgebraicCurve.IsCurveOver.toHasPrincipalDivisors
AlgebraicCurve.IsCurveOver.instFiniteResidue
AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
AlgebraicCurve.Place.instIsLocalHomRestrictInclusion
AlgebraicCurve.Place.kw_ffgc_finiteDimensional_adicCompletion
AlgebraicCurve.Place.kw_ffgc_isScalarTower_integersIntegersCompletion
ModularCurve.KwF4gRRTate.instAlgebraKAdicCompletionIntegers
AlgebraicCurve.Place.kw_ffgc_continuousSMul_adicCompletionComap
AlgebraicCurve.Place.kw_ffgc_isScalarTower_integersCompletionCompletion
instLiesOverSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegersCompletionIdealAsIdeal
attribute [-simp] AlgebraicCurve.Place.CanonicalLocalResidueDataS.mk.sizeOf_spec
AlgebraicCurve.Place.mem_simplePoleSubmodule AlgebraicCurve.Place.coe_uniformizerSubring
ModularCurve.Lg37.Lg37CompletionSection.mk.injEq
AlgebraicCurve.Place.CoefficientFieldSection.mk.injEq
AlgebraicCurve.Place.CanonicalLocalResidueDataS.mk.injEq
ModularCurve.Lg37.Lg37CompletionSection.mk.sizeOf_spec
AlgebraicCurve.Place.CoefficientFieldSection.mk.sizeOf_spec
AlgebraicCurve.Place.poleSubmodule_one AlgebraicCurve.Place.mem_poleSubmodule
AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
AlgebraicCurve.Place.kw_ffgc_adicCompletionComapIntegers_coe
universe u v w
open AlgebraicCurve inLean source · statement
theorem _root_.TwoChartCech.Cover.LaurentChart.residue_eq_kaehlerResidueTerm {k : Type u} [Field
k] {F : Type v} [Field F] [Algebra k F]
[AlgebraicCurve.HasCanonicalLocalResidueKStar k F]
{𝒰 : TwoChartCech.Cover.{u, w} k} (Λ : 𝒰.LaurentChart) (ψ : 𝒰.A01 →ₐ[k] F)
(Φ : Ω[𝒰.A01⁄k] →ₗ[k] Ω[F⁄k])
(hΦ : ∀ s g : 𝒰.A01, Φ (s • KaehlerDifferential.D k 𝒰.A01 g) = ψ s • KaehlerDifferential.D k
F (ψ g))
(Λ' : F →+* LaurentSeries k) (hΛ' : ∀ y : 𝒰.A01, Λ' (ψ y) = Λ.expand y)
(v : AlgebraicCurve.Place k F) [v.DCoordGenerates] [Nontrivial Ω[F⁄k]]
(hΛv : ∀ f : F, f ∈ v.toValuationSubring ↔ Λ' f ∈ (HahnSeries.ofPowerSeries ℤ k).range)
{t₀ : F} (ht₀ : Λ' t₀ = HahnSeries.single 1 1) (η : Ω[𝒰.A01⁄k]) :
Λ.residue η = AlgebraicCurve.kaehlerResidueTerm (Φ η) (AlgebraicCurve.diagonalHom k F 1) v