AlgebraicCurves.Divisors.Proofs.Exists_list_isPrincipal_sub_sum_single_sub_smul_single.AlgebraicCurve.FFRepGlue.exists_list_sum_single_eq
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_list_isPrincipal_sub_sum_single_sub_smul_single
attribute [-instance]
AlgebraicCurve.instHasLocalResidue_of_hasCanonicalLocalResidueK
AlgebraicCurve.instHasCanonicalLocalResidueK_of_hasCanonicalLocalResidueKStar
AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
instIsScalarTowerResidueFieldRestrictPushforward
instAlgebraResidueFieldRestrictPushforward
instIsLocalHomRestrictInclusion
kw_ffgc_finiteDimensional_adicCompletion
kw_ffgc_isScalarTower_integersIntegersCompletion
ModularCurve.KwF4gRRTate.instAlgebraKAdicCompletionIntegers
kw_ffgc_continuousSMul_adicCompletionComap
kw_ffgc_isScalarTower_integersCompletionCompletion
instLiesOverSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegersCompletionIdealAsIdeal
AlgebraicCurve.instHasCanonicalLocalResidueK
instAlgebra_restrictResidueField
instIsScalarTower_restrictResidueField
AlgebraicCurve.instHasLocalResidue
AlgebraicCurve.HasSeparableResidue.of_perfectField_of_isCurveOver
AlgebraicCurve.HasSeparableResidue.of_perfectField
instIsLocalHom_restrictSubringHom
AlgebraicCurve.instHasCanonicalLocalResidueKStar
ModularCurve.KwNo6Pin.isLocalRing_completion
instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
instIsPrimeCenter
instIsFractionRingIntegralClosureAt
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
instIsDedekindDomainIntegralClosureAt
instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
AlgebraicCurve.Place.differentialCoeff_dCoord
AlgebraicCurve.Place.CanonicalLocalResidueDataK.mk.sizeOf_spec
AlgebraicCurve.Place.CanonicalLocalResidueDataK.mk.injEq AlgebraicCurve.adeleSingle_coe
AlgebraicCurve.kaehlerResidueTermKFam_apply AlgebraicCurve.Place.LocalResidueData.mk.injEq
AlgebraicCurve.Place.LocalResidueData.mk.sizeOf_spec 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
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.Place.congrEquiv_symm_apply
AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
universe u v
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFRepGlue
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F]Lean source · full declaration
theorem exists_list_sum_single_eq (hdeg : ∀ v : Place K F, v.deg = 1) :
∀ E : Divisor K F, 0 ≤ E →
∃ l : List (Place K F), (l.map fun v => Finsupp.single v (1 : ℤ)).sum = E ∧ (l.length : ℤ) =
Divisor.degree E := by
classical
intro E
induction E using Finsupp.induction with
| zero => intro _; exact ⟨[], by simp, by simp⟩
| single_add v n E hv hn ih =>
intro hE
have hEv : ∀ w, 0 ≤ (Finsupp.single v n + E) w := fun w => hE w
have hn0 : 0 ≤ n := by
have := hEv v
rw [Finsupp.add_apply, Finsupp.single_eq_same] at this
have hEv0 : E v = 0 := by simpa [Finsupp.mem_support_iff] using hv
omega
have hE' : 0 ≤ E := by
intro w
rcases eq_or_ne w v with rfl | hw
· have hEv0 : E w = 0 := by simpa [Finsupp.mem_support_iff] using hv
simp [hEv0]
· have := hEv w
have hs : (Finsupp.single v n) w = 0 := Finsupp.single_eq_of_ne hw
rw [Finsupp.add_apply, hs, zero_add] at this
simpa using this
obtain ⟨l, hl, hlen⟩ := ih hE'
refine ⟨List.replicate n.toNat v ++ l, ?_, ?_⟩
· rw [List.map_append, List.sum_append, hl, List.map_replicate, List.sum_replicate, ←
Finsupp.smul_single_one v n]
congr 1
rw [← natCast_zsmul, Int.toNat_of_nonneg hn0]
· rw [List.length_append, List.length_replicate, Nat.cast_add, hlen, map_add,
Divisor.degree_single, hdeg, Nat.cast_one,
mul_one, Int.toNat_of_nonneg hn0]