truncT/singleT/mulInto/nuL: the truncation and multiplication kit (serre-duality-tails)

Unit: serre-duality-tails (docs/design/serre-duality-tails.md §3 D1/D3, §5.1, §6 P1).

• truncAt/truncT: Miranda's truncation lattice t^{D₁}_{D₂} : T[D₁] → T[D₂] for D₁ ≤ D₂ (coarser quotient; surjective), and its compatibility with alphaL (Miranda Problem C).
• singleT: the test-vector tail at a single point (used by the injectivity/Lemma-3.6 witnesses).
• mulIntoAt/mulInto: Miranda's t ∘ μ_f as ONE uniform map T D →ₗ[ℂ] T E, linear in f (no f ≠ 0 needed), surjective when f ≠ 0 (Problem B: compatibility with alphaL).
• nuL: the packaging ↥(LinSys C) →ₗ[ℂ] (T (A - C) →ₗ[ℂ] T A) Lemma 3.4's pair map is built from, plus the μ_{1/f} inversion identity nuL_mulInto_inv the surjectivity endgame needs.

ordGe monotonicity (the engine behind truncAt/mulIntoAt's well-definedness)

theorem RS.TailDuality.ordGe_mono {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (p : X) {m₁ m₂ : ℤ} (h : m₂ ≤ m₁) : Cech.ordGe p m₁ ≤ Cech.ordGe p m₂

truncAt/truncT (D1)

noncomputable def RS.TailDuality.truncAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (p : X) {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) : LaurentTail.TailAt p D₁ →ₗ[ℂ] LaurentTail.TailAt p D₂

Miranda's t^{D₁}_{D₂} at a single point: the coarsening TailAt p D₁ →ₗ TailAt p D₂.

Equations

• RS.TailDuality.truncAt p h = (RS.Cech.ordGe p (-D₁ p)).mapQ (RS.Cech.ordGe p (-D₂ p)) LinearMap.id ⋯

@[simp]

theorem RS.TailDuality.truncAt_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (p : X) {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) (ψ : MeroGermOn X (chartAt ℂ p).source) : (truncAt p h) ((LaurentTail.TailAt.mk p D₁) ψ) = (LaurentTail.TailAt.mk p D₂) ψ

theorem RS.TailDuality.truncAt_surjective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (p : X) {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) : Function.Surjective ⇑(truncAt p h)

noncomputable def RS.TailDuality.truncT {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) : LaurentTail.T D₁ →ₗ[ℂ] LaurentTail.T D₂

Miranda's t^{D₁}_{D₂} : T[D₁] → T[D₂], assembled pointwise.

Equations

• RS.TailDuality.truncT h = { toFun := fun (τ : RS.LaurentTail.T D₁) => DFinsupp.mapRange (fun (p : X) => ⇑(RS.TailDuality.truncAt p h)) ⋯ τ, map_add' := ⋯, map_smul' := ⋯ }

theorem RS.TailDuality.truncT_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) (τ : LaurentTail.T D₁) (p : X) : ((truncT h) τ) p = (truncAt p h) (τ p)

theorem RS.TailDuality.truncT_surjective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) : Function.Surjective ⇑(truncT h)

theorem RS.TailDuality.truncT_alpha {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [DecidableEq X] [CompactSpace X] [ConnectedSpace X] {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) (f : Mero X) : (truncT h) ((LaurentTail.alphaL D₁) f) = (LaurentTail.alphaL D₂) f

singleT (the test-vector tails)

noncomputable def RS.TailDuality.singleT {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [DecidableEq X] (p : X) (D : Divisor X) (ψ : MeroGermOn X (chartAt ℂ p).source) : LaurentTail.T D

A single-point test tail: the class of ψ at p, zero elsewhere.

Equations

• RS.TailDuality.singleT p D ψ = DFinsupp.single p ((RS.LaurentTail.TailAt.mk p D) ψ)

@[simp]

theorem RS.TailDuality.singleT_apply_self {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [DecidableEq X] (p : X) (D : Divisor X) (ψ : MeroGermOn X (chartAt ℂ p).source) : (singleT p D ψ) p = (LaurentTail.TailAt.mk p D) ψ

theorem RS.TailDuality.singleT_apply_of_ne {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [DecidableEq X] {p q : X} (hqp : q ≠ p) (D : Divisor X) (ψ : MeroGermOn X (chartAt ℂ p).source) : (singleT p D ψ) q = 0

theorem RS.TailDuality.singleT_eq_zero_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [DecidableEq X] (p : X) (D : Divisor X) (ψ : MeroGermOn X (chartAt ℂ p).source) : singleT p D ψ = 0 ↔ -↑(D p) ≤ ψ.ord p

@[simp]

theorem RS.TailDuality.truncT_singleT {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [DecidableEq X] {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) : (truncT h) (singleT p D₁ ψ) = singleT p D₂ ψ

mulIntoAt/mulInto (D3): Miranda's t ∘ μ_f, uniform in f

theorem RS.TailDuality.mulIntoAt_bound_computation {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (p : X) (f : Mero X) {D E : Divisor X} (hf : ↑(D p - E p) ≤ MeroGermOn.ord f p) (ψ : MeroGermOn X (chartAt ℂ p).source) (hψ : ↑(-D p) ≤ ψ.ord p) : ↑(-E p) ≤ ((MeroGermOn.restrict ⋯) f * ψ).ord p

noncomputable def RS.TailDuality.mulIntoAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : Mero X) (p : X) {D E : Divisor X} (hf : ↑(D p - E p) ≤ MeroGermOn.ord f p) : LaurentTail.TailAt p D →ₗ[ℂ] LaurentTail.TailAt p E

Miranda's μ_f composed with truncation, at a single point: TailAt p D →ₗ TailAt p E for f whose order at p is bounded below by D p - E p.

Equations

• RS.TailDuality.mulIntoAt f p hf = (RS.Cech.ordGe p (-D p)).mapQ (RS.Cech.ordGe p (-E p)) (LinearMap.mulLeft ℂ ((RS.MeroGermOn.restrict ⋯) f)) ⋯

@[simp]

theorem RS.TailDuality.mulIntoAt_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : Mero X) (p : X) {D E : Divisor X} (hf : ↑(D p - E p) ≤ MeroGermOn.ord f p) (ψ : MeroGermOn X (chartAt ℂ p).source) : (mulIntoAt f p hf) ((LaurentTail.TailAt.mk p D) ψ) = (LaurentTail.TailAt.mk p E) ((MeroGermOn.restrict ⋯) f * ψ)

theorem RS.TailDuality.mulIntoAt_surjective {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] {f : Mero X} (hf0 : f ≠ 0) [ConnectedSpace X] (p : X) {D E : Divisor X} (hf : ↑(D p - E p) ≤ MeroGermOn.ord f p) : Function.Surjective ⇑(mulIntoAt f p hf)

noncomputable def RS.TailDuality.mulInto {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : Mero X) {D E : Divisor X} (hf : ∀ (p : X), ↑(D p - E p) ≤ MeroGermOn.ord f p) : LaurentTail.T D →ₗ[ℂ] LaurentTail.T E

Miranda's t ∘ μ_f : T D →ₗ T E, uniform in f (linear in f, §3 D3).

Equations

• RS.TailDuality.mulInto f hf = { toFun := fun (τ : RS.LaurentTail.T D) => DFinsupp.mapRange (fun (p : X) => ⇑(RS.TailDuality.mulIntoAt f p ⋯)) ⋯ τ, map_add' := ⋯, map_smul' := ⋯ }

theorem RS.TailDuality.mulInto_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : Mero X) {D E : Divisor X} (hf : ∀ (p : X), ↑(D p - E p) ≤ MeroGermOn.ord f p) (τ : LaurentTail.T D) (p : X) : ((mulInto f hf) τ) p = (mulIntoAt f p ⋯) (τ p)

theorem RS.TailDuality.mulInto_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f g : Mero X) {D E : Divisor X} (hf : ∀ (p : X), ↑(D p - E p) ≤ MeroGermOn.ord f p) (hg : ∀ (p : X), ↑(D p - E p) ≤ MeroGermOn.ord g p) (hfg : ∀ (p : X), ↑(D p - E p) ≤ MeroGermOn.ord (f + g) p) : mulInto (f + g) hfg = mulInto f hf + mulInto g hg

theorem RS.TailDuality.mulInto_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (c : ℂ) (f : Mero X) {D E : Divisor X} (hf : ∀ (p : X), ↑(D p - E p) ≤ MeroGermOn.ord f p) (hcf : ∀ (p : X), ↑(D p - E p) ≤ MeroGermOn.ord (c • f) p) : mulInto (c • f) hcf = c • mulInto f hf

theorem RS.TailDuality.mulInto_alpha {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [DecidableEq X] [CompactSpace X] [ConnectedSpace X] (f : Mero X) {D E : Divisor X} (hf : ∀ (p : X), ↑(D p - E p) ≤ MeroGermOn.ord f p) (g : Mero X) : (mulInto f hf) ((LaurentTail.alphaL D) g) = (LaurentTail.alphaL E) (f * g)

theorem RS.TailDuality.mulInto_surjective {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] {f : Mero X} (hf0 : f ≠ 0) [ConnectedSpace X] {D E : Divisor X} (hf : ∀ (p : X), ↑(D p - E p) ≤ MeroGermOn.ord f p) : Function.Surjective ⇑(mulInto f hf)

LinSys/Mero.ord bookkeeping helpers

theorem RS.TailDuality.LinSys.divisor_ge {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [ConnectedSpace X] {C : Divisor X} {f : Mero X} (hf : f ∈ LinSys C) (hf0 : f ≠ 0) (p : X) : -C p ≤ (divisor f) p

theorem RS.TailDuality.Mero.ord_eq_divisor {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [ConnectedSpace X] {f : Mero X} (hf : f ≠ 0) (p : X) : MeroGermOn.ord f p = ↑((divisor f) p)

nuL

theorem RS.TailDuality.nu_bound {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (A C : Divisor X) (f : ↥(LinSys C)) (p : X) : ↑((A - C) p - A p) ≤ MeroGermOn.ord (↑f) p

noncomputable def RS.TailDuality.nuL {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] (A C : Divisor X) [ConnectedSpace X] : ↥(LinSys C) →ₗ[ℂ] LaurentTail.T (A - C) →ₗ[ℂ] LaurentTail.T A

Miranda's μ_f packaged uniformly across f ∈ L(C) into the FIXED target T A (the key linearity-restoring trick, §3 D3).

Equations

• RS.TailDuality.nuL A C = { toFun := fun (f : ↥(RS.LinSys C)) => RS.TailDuality.mulInto ↑f ⋯, map_add' := ⋯, map_smul' := ⋯ }

theorem RS.TailDuality.nuL_apply {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] (A C : Divisor X) [ConnectedSpace X] (f : ↥(LinSys C)) : (nuL A C) f = mulInto ↑f ⋯

theorem RS.TailDuality.nuL_alpha {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [DecidableEq X] (A C : Divisor X) [CompactSpace X] [ConnectedSpace X] (f : ↥(LinSys C)) (g : Mero X) : ((nuL A C) f) ((LaurentTail.alphaL (A - C)) g) = (LaurentTail.alphaL A) (↑f * g)

theorem RS.TailDuality.nuL_surjective {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] (A C : Divisor X) [ConnectedSpace X] {f : ↥(LinSys C)} (hf0 : ↑f ≠ 0) : Function.Surjective ⇑((nuL A C) f)

theorem RS.TailDuality.sub_divisor_le {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (A C : Divisor X) [ConnectedSpace X] {f : ↥(LinSys C)} (hf0 : ↑f ≠ 0) : A - C - divisor ↑f ≤ A

theorem RS.TailDuality.nuL_mulInto_inv {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (A C : Divisor X) [ConnectedSpace X] {f : ↥(LinSys C)} (hf0 : ↑f ≠ 0) (hinv : ∀ (p : X), ↑((A - C - divisor ↑f) p - (A - C) p) ≤ MeroGermOn.ord (↑f)⁻¹ p) (τ' : LaurentTail.T (A - C - divisor ↑f)) : ((nuL A C) f) ((mulInto (↑f)⁻¹ hinv) τ') = (truncT ⋯) τ'

The μ_{1/f} inversion identity (endgame step): inverting f and truncating recovers the plain truncation.