The truncation map α_D and H¹Tail(D) (laurent-tails, design §2 D3, §4.2)

Unit: laurent-tails (docs/design/laurent-tails.md).

• alphaFinset D f: a Finset witness containing every point where α_D f's tail component is possibly nonzero (D.support together with f's pole set).
• alpha/alphaL: Miranda's truncation α_D : ℳ X → T[D], α_D f's class at p is the chart restriction of f mod ordGe p (-(D p)) — at every p, not just on the witness Finset (alpha_apply, exported per docs/requests/laurent-tails.md's serre-duality-tails ask).
• ker_alphaL_eq_linSys: Miranda's L(D) = ker(α_D) (PDF 192).
• H1Tail D := T D ⧸ range(alphaL D): Miranda's own definition of H¹(D) (the comparison to Cech.H1 D is Comparison.lean's job).

alphaFinset, alpha, alphaL

noncomputable def RS.LaurentTail.alphaFinset {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (f : Mero X) : Finset X

A Finset witness for α_D f's (possibly) nonzero locus: D's own (finite, compactness) support, together with f's pole set (finite, compactness + connectedness) when f ≠ 0.

Equations

• RS.LaurentTail.alphaFinset D f = ⋯.toFinset ∪ if hf : f = 0 then ∅ else ⋯.toFinset

theorem RS.LaurentTail.not_mem_alphaFinset {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (f : Mero X) {p : X} (hp : p ∉ alphaFinset D f) : -↑(D p) ≤ MeroGermOn.ord f p

Every point outside the witness Finset is a genuine "good" point: f's chart-restriction class there already lies in L(D)'s local bound.

noncomputable def RS.LaurentTail.alpha {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (f : Mero X) : T D

Miranda's truncation α_D, assembled from the witness Finset (§2 D3).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RS.LaurentTail.alpha_apply {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (f : Mero X) (p : X) : (alpha D f) p = (TailAt.mk p D) ((MeroGermOn.restrict ⋯) f)

alpha D f's value at every point p (not just the witness Finset) is the chart restriction of f mod ordGe p (-(D p)) — requested by serre-duality-tails (docs/requests/laurent-tails.md).

theorem RS.LaurentTail.alpha_apply_eq_zero_iff {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (f : Mero X) (p : X) : (alpha D f) p = 0 ↔ -↑(D p) ≤ MeroGermOn.ord f p

noncomputable def RS.LaurentTail.alphaL {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) : Mero X →ₗ[ℂ] T D

α_D : ℳ X →ₗ[ℂ] T D, Miranda's truncation map.

Equations

• RS.LaurentTail.alphaL D = { toFun := RS.LaurentTail.alpha D, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem RS.LaurentTail.alphaL_apply {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (f : Mero X) : (alphaL D) f = alpha D f

theorem RS.LaurentTail.ker_alphaL_eq_linSys {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) : (alphaL D).ker = LinSys D

Miranda PDF 192: L(D) = ker(α_D).

H1Tail D

noncomputable def RS.LaurentTail.H1Tail {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) : Type u_1

Miranda's H¹(D) := T[D]/α_D(ℳ) (PDF 192-193). The comparison to Cech.H1 D (RS.Cech.H1) is Comparison.lean's job.

Equations

• RS.LaurentTail.H1Tail D = (RS.LaurentTail.T D ⧸ (RS.LaurentTail.alphaL D).range)

@[instance_reducible]

noncomputable instance RS.LaurentTail.instAddCommGroupH1Tail {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) : AddCommGroup (H1Tail D)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance RS.LaurentTail.instModuleH1Tail {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) : Module ℂ (H1Tail D)

Equations

• RS.LaurentTail.instModuleH1Tail D = { smul := RS.LaurentTail.instModuleH1Tail._aux_1 D, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

noncomputable def RS.LaurentTail.H1Tail.mk {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) : T D →ₗ[ℂ] H1Tail D

The quotient map onto H¹Tail(D).

Equations

• RS.LaurentTail.H1Tail.mk D = (RS.LaurentTail.alphaL D).range.mkQ

theorem RS.LaurentTail.H1Tail.mk_surjective {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) : Function.Surjective ⇑(mk D)

theorem RS.LaurentTail.H1Tail.mk_eq_zero_iff {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (τ : T D) : (mk D) τ = 0 ↔ τ ∈ (alphaL D).range