Ell_nsmul_eq_card_of_flagAdaptedBasisAt.lean

theorem ord_pow (v : Place K F) {x : F} (hx : x ≠ 0) (j : ℕ) :
    v.ord (x ^ j) = j * v.ord x

theorem pow_mul_mem_lSpace_nsmul (x : F) (D : Divisor K F)
    (hD : ∀ v : Place K F, D v = max 0 (-v.ord x))
    {y : F} {k : ℕ} (hy : y ∈ LSpace (k • D)) (j : ℕ) :
    x ^ j * y ∈ LSpace ((j + k) • D)

instance fintypeIdxFiber {d' : ℕ} (e : Fin d' → ℕ) (m : ℕ) (σ : Fin d') :
    Fintype {j : ℕ // j + e σ ≤ m}

instance fintypeIdx {d' : ℕ} (e : Fin d' → ℕ) (m : ℕ) :
    Fintype {p : Fin d' × ℕ // p.2 + e p.1 ≤ m}

theorem card_idx {d' : ℕ} (e : Fin d' → ℕ) (m : ℕ) :
    Fintype.card {p : Fin d' × ℕ // p.2 + e p.1 ≤ m}
      = ∑ σ ∈ (Finset.univ : Finset (Fin d')).filter (fun σ => e σ ≤ m), (m + 1 - e σ) := by
  have equiv : {p : Fin d' × ℕ // p.2 + e p.1 ≤ m}
      ≃ Σ σ : Fin d', {j : ℕ // j + e σ ≤ m} := {
    toFun := fun ⟨⟨σ, j⟩, h⟩ => ⟨σ, j, h⟩
    invFun := fun ⟨σ, j, h⟩ => ⟨⟨σ, j⟩, h⟩
    left_inv := fun _ => rfl
    right_inv := fun _ => rfl }
  rw [Fintype.card_congr equiv, Fintype.card_sigma]
  rw [show (∑ σ ∈ Finset.univ.filter (fun σ => e σ ≤ m), (m + 1 - e σ))
        = ∑ σ : Fin d', if e σ ≤ m then (m + 1 - e σ) else 0 from
      Finset.sum_filter _ _]
  refine Finset.sum_congr rfl fun σ _ => ?_
  split_ifs with h
  · have fequiv : {j : ℕ // j + e σ ≤ m} ≃ Fin (m + 1 - e σ) := {
      toFun := fun ⟨j, hj⟩ => ⟨j, by omega⟩
      invFun := fun ⟨j, hj⟩ => ⟨j, by omega⟩
      left_inv := fun _ => rfl
      right_inv := fun _ => rfl }
    rw [Fintype.card_congr fequiv, Fintype.card_fin]
  · have : IsEmpty {j : ℕ // j + e σ ≤ m} := ⟨fun ⟨j, hj⟩ => h (by omega)⟩
    exact Fintype.card_eq_zero

theorem _root_.AlgebraicCurve.ell_nsmul_eq_card_of_flagAdaptedBasisAt {K F : Type*} [Field K]
  [Field F] [Algebra K F]
    (x : F) (D : Divisor K F) (hD : ∀ v : Place K F, D v = max 0 (-v.ord x))
    {d' : ℕ} (y : Fin d' → F) (e : Fin d' → ℕ)
    (hyL : ∀ σ, y σ ∈ LSpace ((e σ) • D))
    (m : ℕ) [FiniteDimensional K ↥(LSpace (m • D))]
    (hspan : (LSpace (m • D) : Submodule K F)
      ≤ Submodule.span K {z | ∃ σ j, j + e σ ≤ m ∧ z = x ^ j * y σ})
    (hLI : LinearIndependent K
      (fun p : {p : Fin d' × ℕ // p.2 + e p.1 ≤ m} => x ^ p.val.2 * y p.val.1)) :
    ell (m • D)
      = ∑ σ ∈ (Finset.univ : Finset (Fin d')).filter (fun σ => e σ ≤ m), (m + 1 - e σ) := by
  let : Fintype {p : Fin d' × ℕ // p.2 + e p.1 ≤ m} := PDAux2Fae.fintypeIdx e m
  have hD0 : ∀ v, 0 ≤ D v := fun v => by rw [hD v]; exact le_max_left _ _
  have hmem : ∀ p : {p : Fin d' × ℕ // p.2 + e p.1 ≤ m},
      x ^ p.val.2 * y p.val.1 ∈ LSpace (m • D) := fun ⟨⟨σ, j⟩, hp⟩ =>
    lSpace_mono (fun v => by
        simp only [Finsupp.smul_apply]
        exact nsmul_le_nsmul_left (hD0 v) hp)
      (PDAux2Fae.pow_mul_mem_lSpace_nsmul x D hD (hyL σ) j)
  have hspanEq : Submodule.span K (Set.range fun p : {p : Fin d' × ℕ // p.2 + e p.1 ≤ m}
        => x ^ p.val.2 * y p.val.1) = LSpace (m • D) := by
    apply le_antisymm
    · rw [Submodule.span_le]; rintro _ ⟨p, rfl⟩; exact hmem p
    · refine le_trans hspan (Submodule.span_mono ?_)
      rintro _ ⟨σ, j, hσj, rfl⟩; exact ⟨⟨(σ, j), hσj⟩, rfl⟩
  calc ell (m • D) = Module.finrank K (LSpace (m • D)) := rfl
    _ = Module.finrank K
          (Submodule.span K (Set.range fun p : {p : Fin d' × ℕ // p.2 + e p.1 ≤ m}
            => x ^ p.val.2 * y p.val.1)) := by rw [hspanEq]
    _ = Fintype.card {p : Fin d' × ℕ // p.2 + e p.1 ≤ m} := finrank_span_eq_card hLI
    _ = _ := PDAux2Fae.card_idx e m