feat: define the index of a linear map (leanprover-community#39930)

And add some basic API.

Written at the ICERM workshop "Techniques and Tools for the Formalization of Analysis".

Co-authored-by: Jon Bannon <jbannon@siena.edu>

Author: 2 people

Mathlib.lean

@@ -303,7 +303,8 @@ public import Mathlib.Algebra.EuclideanDomain.Basic
 public import Mathlib.Algebra.EuclideanDomain.Defs
 public import Mathlib.Algebra.EuclideanDomain.Field
 public import Mathlib.Algebra.EuclideanDomain.Int
-public import Mathlib.Algebra.Exact
+public import Mathlib.Algebra.Exact.Basic
+public import Mathlib.Algebra.Exact.Sequence
 public import Mathlib.Algebra.Expr
 public import Mathlib.Algebra.Field.Action.ConjAct
 public import Mathlib.Algebra.Field.Basic
@@ -781,6 +782,7 @@ public import Mathlib.Algebra.Module.LinearMap.Defs
 public import Mathlib.Algebra.Module.LinearMap.DivisionRing
 public import Mathlib.Algebra.Module.LinearMap.End
 public import Mathlib.Algebra.Module.LinearMap.FiniteRange
+public import Mathlib.Algebra.Module.LinearMap.Index
 public import Mathlib.Algebra.Module.LinearMap.Polynomial
 public import Mathlib.Algebra.Module.LinearMap.Prod
 public import Mathlib.Algebra.Module.LinearMap.Rat

Mathlib/Algebra/BigOperators/Fin.lean

@@ -775,3 +775,28 @@ alias alternatingSum_eq_finset_sum := alternatingSum_eq_finsetSum
 alias alternatingProd_eq_finset_prod := alternatingProd_eq_finsetProd
 
 end List
+
+/-- This is a classic "telescoping sum" lemma. It says:
+`r₀ - (r₀ + r₁) + (r₁ + r₂) - (r₂+ r₃) + ⋯ ± (rₙ₋₁ + rₙ) ∓ rₙ = 0`.
+
+The chosen spelling, which gives definitional power over `d`, is influenced by downstream
+applications such as `Module.sum_neg_one_pow_finrank_eq_zero_of_exact`. -/
+lemma Fin.sum_neg_one_pow_eq_zero {α : Type*} [AddCommGroup α]
+    {n : ℕ} (d : Fin (n + 2) → α) (r : Fin (n + 1) → α)
+    (h_first : d 0 = r 0)
+    (h_mid : ∀ i : Fin n, d i.succ.castSucc = r i.castSucc + r i.succ)
+    (h_last : d (Fin.last _) = r (Fin.last _)) :
+    ∑ i, (-1) ^ i.val • d i = 0 := by
+  have h₁ : ∑ i : Fin (n + 2), (-1 : ℤ) ^ i.val • d i =
+      d 0 +
+      ∑ i : Fin n, (-1 : ℤ) ^ (i.val + 1) • (d (Fin.castSucc i).succ) +
+      (-1 : ℤ) ^ (n + 1) • d (Fin.last (n + 1)) := by
+    rw [Fin.sum_univ_succ, Fin.sum_univ_castSucc]
+    simp [add_assoc]
+  have h₂ : ∑ i : Fin n, (-1 : ℤ) ^ (i.val + 1) • (r (Fin.castSucc i) + r (Fin.succ i)) =
+      ∑ i : Fin n, (-1 : ℤ) ^ (i.val + 1) • r (Fin.castSucc i) +
+      ∑ i : Fin n, (-1 : ℤ) ^ (i.val + 1) • r (Fin.succ i) := by
+    simp_rw [zsmul_add, Finset.sum_add_distrib]
+  have h₃ := Fin.sum_univ_castSucc fun i ↦ (-1 : ℤ) ^ i.val • r i
+  simp_all [Fin.sum_univ_succ, pow_succ']
+  grind

Mathlib/Algebra/Category/ModuleCat/Kernels.lean

@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Algebra.Category.ModuleCat.EpiMono
 public import Mathlib.CategoryTheory.ConcreteCategory.Elementwise
-public import Mathlib.Algebra.Exact
+public import Mathlib.Algebra.Exact.Basic
 public import Mathlib.LinearAlgebra.Isomorphisms
 
 /-!

Mathlib/Algebra/Exact.lean Mathlib/Algebra/Exact/Basic.leanMathlib/Algebra/Exact.lean renamed to Mathlib/Algebra/Exact/Basic.lean

@@ -0,0 +1,124 @@
+/-
+Copyright (c) 2026 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Nash, Jon Bannon
+-/
+module
+
+public import Mathlib.Algebra.BigOperators.Fin
+public import Mathlib.Algebra.Exact.Basic
+public import Mathlib.LinearAlgebra.Dimension.Constructions
+public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
+
+/-! # Exactness of sequences
+
+In this file we provide some API for handling exact sequences.
+
+## Main definitions / results:
+
+* `Module.sum_neg_one_pow_finrank_eq_zero_of_exact`: the Euler characteristic of a finite exact
+  sequence is zero.
+
+## TODO
+
+Write a simproc to generate unrolled, universe-polymorphic versions of
+`Module.sum_neg_one_pow_finrank_eq_zero_of_exact` on the fly and so obviate the need for
+`Module.sum_neg_one_pow_finrank_eq_zero_of_exact_six`.
+
+-/
+
+universe u₀ u₁ u₂ u₃ u₄ u₅
+
+namespace Module
+
+open Function
+
+variable {k : Type*} [DivisionRing k]
+
+/-- The Euler characteristic of a finite exact sequence is zero. -/
+public lemma sum_neg_one_pow_finrank_eq_zero_of_exact {n : ℕ} (V : Fin (n + 2) → Type*)
+    [∀ i, AddCommGroup (V i)] [∀ i, Module k (V i)] [∀ i, FiniteDimensional k (V i)]
+    (f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ)
+    (inj : Injective (f 0))
+    (h_exact : ∀ i : Fin n, Exact (f i.castSucc) (f i.succ))
+    (surj : Surjective (f (Fin.last _))) :
+    ∑ i, (-1) ^ i.val * (finrank k (V i) : ℤ) = 0 := by
+  replace inj := LinearMap.finrank_range_of_inj inj
+  replace surj := LinearMap.range_eq_top.mpr surj
+  simp_rw [← smul_eq_mul]
+  refine Fin.sum_neg_one_pow_eq_zero _ (fun i ↦ finrank k (f i).range) ?_ (fun i ↦ ?_) ?_
+  · aesop
+  · grind [(h_exact i).linearMap_ker_eq, (f i.succ).finrank_range_add_finrank_ker]
+  · grind [finrank_top]
+
+/- An unrolled version of `Module.sum_neg_one_pow_finrank_eq_zero_of_exact`. This is an auxiliary
+lemma en route to `Module.sum_neg_one_pow_finrank_eq_zero_of_exact_six`. -/
+private lemma sum_neg_one_pow_finrank_eq_zero_of_exact_six_aux {V₀ V₁ V₂ V₃ V₄ V₅ : Type u₀}
+    [AddCommGroup V₀] [Module k V₀] [FiniteDimensional k V₀]
+    [AddCommGroup V₁] [Module k V₁] [FiniteDimensional k V₁]
+    [AddCommGroup V₂] [Module k V₂] [FiniteDimensional k V₂]
+    [AddCommGroup V₃] [Module k V₃] [FiniteDimensional k V₃]
+    [AddCommGroup V₄] [Module k V₄] [FiniteDimensional k V₄]
+    [AddCommGroup V₅] [Module k V₅] [FiniteDimensional k V₅]
+    (f₀ : V₀ →ₗ[k] V₁) (f₁ : V₁ →ₗ[k] V₂) (f₂ : V₂ →ₗ[k] V₃) (f₃ : V₃ →ₗ[k] V₄) (f₄ : V₄ →ₗ[k] V₅)
+    (inj : Injective f₀)
+    (exact₁ : Exact f₀ f₁)
+    (exact₂ : Exact f₁ f₂)
+    (exact₃ : Exact f₂ f₃)
+    (exact₄ : Exact f₃ f₄)
+    (surj : Surjective f₄) :
+    (finrank k V₀ : ℤ) - finrank k V₁ + finrank k V₂ -
+      finrank k V₃ + finrank k V₄ - finrank k V₅ = 0 := by
+  letI Vs := ![V₀, V₁, V₂, V₃, V₄, V₅]
+  letI (i : Fin 6) : AddCommGroup (Vs i) := match i with
+  | 0 => ‹_› | 1 => ‹_› | 2 => ‹_› | 3 => ‹_› | 4 => ‹_› | 5 => ‹_›
+  letI (i : Fin 6) : Module k (Vs i) := match i with
+  | 0 => ‹_› | 1 => ‹_› | 2 => ‹_› | 3 => ‹_› | 4 => ‹_› | 5 => ‹_›
+  have (i : Fin 6) : FiniteDimensional k (Vs i) := match i with
+  | 0 => ‹_› | 1 => ‹_› | 2 => ‹_› | 3 => ‹_› | 4 => ‹_› | 5 => ‹_›
+  letI fs (i : Fin 5) : Vs i.castSucc →ₗ[k] Vs i.succ := match i with
+  | 0 => f₀ | 1 => f₁ | 2 => f₂ | 3 => f₃ | 4 => f₄
+  simpa [Fin.sum_univ_six] using Module.sum_neg_one_pow_finrank_eq_zero_of_exact Vs fs inj
+    (fun i ↦ by fin_cases i; exacts [exact₁, exact₂, exact₃, exact₄]) surj
+
+/-- This is an unrolled, universe-polymorphic version of
+`Module.sum_neg_one_pow_finrank_eq_zero_of_exact`. This special case exists because of the role that
+this lemma plays in the proof of `LinearMap.index_comp`.
+
+In theory one could write a `simproc` which conjured up this lemma for a sequence of any length and
+then one would not need to have this special-case lemma at all. -/
+public lemma sum_neg_one_pow_finrank_eq_zero_of_exact_six
+    {V₀ : Type u₀} [AddCommGroup V₀] [Module k V₀] [FiniteDimensional k V₀]
+    {V₁ : Type u₁} [AddCommGroup V₁] [Module k V₁] [FiniteDimensional k V₁]
+    {V₂ : Type u₂} [AddCommGroup V₂] [Module k V₂] [FiniteDimensional k V₂]
+    {V₃ : Type u₃} [AddCommGroup V₃] [Module k V₃] [FiniteDimensional k V₃]
+    {V₄ : Type u₄} [AddCommGroup V₄] [Module k V₄] [FiniteDimensional k V₄]
+    {V₅ : Type u₅} [AddCommGroup V₅] [Module k V₅] [FiniteDimensional k V₅]
+    (f₀ : V₀ →ₗ[k] V₁) (f₁ : V₁ →ₗ[k] V₂) (f₂ : V₂ →ₗ[k] V₃) (f₃ : V₃ →ₗ[k] V₄) (f₄ : V₄ →ₗ[k] V₅)
+    (inj : Injective f₀)
+    (exact₁ : Exact f₀ f₁)
+    (exact₂ : Exact f₁ f₂)
+    (exact₃ : Exact f₂ f₃)
+    (exact₄ : Exact f₃ f₄)
+    (surj : Surjective f₄) :
+    (finrank k V₀ : ℤ) - finrank k V₁ + finrank k V₂ -
+      finrank k V₃ + finrank k V₄ - finrank k V₅ = 0 := by
+  let W₀ := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅} V₀
+  let W₁ := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅} V₁
+  let W₂ := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅} V₂
+  let W₃ := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅} V₃
+  let W₄ := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅} V₄
+  let W₅ := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅} V₅
+  let g₀ : W₀ →ₗ[k] W₁ := ULift.moduleEquiv.symm.toLinearMap ∘ₗ f₀ ∘ₗ ULift.moduleEquiv.toLinearMap
+  let g₁ : W₁ →ₗ[k] W₂ := ULift.moduleEquiv.symm.toLinearMap ∘ₗ f₁ ∘ₗ ULift.moduleEquiv.toLinearMap
+  let g₂ : W₂ →ₗ[k] W₃ := ULift.moduleEquiv.symm.toLinearMap ∘ₗ f₂ ∘ₗ ULift.moduleEquiv.toLinearMap
+  let g₃ : W₃ →ₗ[k] W₄ := ULift.moduleEquiv.symm.toLinearMap ∘ₗ f₃ ∘ₗ ULift.moduleEquiv.toLinearMap
+  let g₄ : W₄ →ₗ[k] W₅ := ULift.moduleEquiv.symm.toLinearMap ∘ₗ f₄ ∘ₗ ULift.moduleEquiv.toLinearMap
+  have := sum_neg_one_pow_finrank_eq_zero_of_exact_six_aux g₀ g₁ g₂ g₃ g₄
+    (inj := by simpa [g₀]) (surj := by simpa [g₄])
+  simp only [W₀, W₁, W₂, W₃, W₄, W₅, finrank_ulift] at this
+  apply this <;>
+  simpa only [g₀, g₁, g₂, g₃, g₄, LinearEquiv.postcomp_exact_iff_exact,
+    LinearEquiv.conj_symm_exact_iff_exact, LinearEquiv.precomp_exact_iff_exact]
+
+end Module

Mathlib/Algebra/Exact/Sequence.lean

@@ -5,7 +5,7 @@ Authors: Christian Merten
 -/
 module
 
-public import Mathlib.Algebra.Exact
+public import Mathlib.Algebra.Exact.Basic
 
 /-!
 # The five lemma in terms of modules

Mathlib/Algebra/FiveLemma.lean

@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Algebra.Category.Grp.Abelian
 public import Mathlib.Algebra.Category.Grp.Kernels
-public import Mathlib.Algebra.Exact
+public import Mathlib.Algebra.Exact.Basic
 public import Mathlib.Algebra.Homology.ShortComplex.ShortExact
 public import Mathlib.GroupTheory.QuotientGroup.Finite
 

Mathlib/Algebra/Homology/ShortComplex/Ab.lean

@@ -5,7 +5,7 @@ Authors: Scott Carnahan
 -/
 module
 
-public import Mathlib.Algebra.Exact
+public import Mathlib.Algebra.Exact.Basic
 public import Mathlib.Algebra.Lie.Cochain
 
 /-!

Mathlib/Algebra/Lie/Extension.lean

@@ -0,0 +1,134 @@
+/-
+Copyright (c) 2026 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Nash
+-/
+module
+
+public import Mathlib.Algebra.Exact.Sequence
+public import Mathlib.Algebra.Module.LinearMap.Defs
+public import Mathlib.Algebra.Module.Submodule.Map
+public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
+
+/-!
+# The index of a linear map
+
+In this file we define the index of a linear map and provide some basic API.
+
+## Main definitions / results:
+
+* `LinearMap.index`: the index of a linear map, with sign convention `index = dim ker - dim coker`.
+* `LinearMap.index_comp`: the index is additive under composition.
+
+-/
+
+noncomputable section
+
+namespace LinearMap
+
+open Function Module
+
+variable {M N : Type*} [AddCommGroup M] [AddCommGroup N]
+
+section Ring
+
+variable {R : Type*} [Ring R] [Module R M] [Module R N] (f : M →ₗ[R] N)
+
+/-- The index of a linear map with sign convention `index = dim ker - dim coker`.
+
+In the case that either the kernel or cokernel has infinite rank, the value is junk. -/
+public def index : ℤ := finrank R f.ker - finrank R (N ⧸ f.range)
+
+variable {f}
+
+public lemma index_eq_finrank_sub :
+    f.index = finrank R f.ker - finrank R (N ⧸ f.range) := by
+  rfl
+
+@[nontriviality] public lemma index_of_subsingleton [Subsingleton R] :
+    f.index = 0 := by
+  simp [index_eq_finrank_sub]
+
+@[simp] public lemma index_zero :
+    (0 : M →ₗ[R] N).index = finrank R M - finrank R N := by
+  rw [index_eq_finrank_sub, ker_zero, range_zero]
+  simpa using (Submodule.quotEquivOfEqBot _ rfl).finrank_eq
+
+public lemma index_of_injective [Nontrivial R] (hf : Injective f) :
+    f.index = - finrank R (N ⧸ f.range) := by
+  simpa [index_eq_finrank_sub] using ker_eq_bot.2 hf ▸ finrank_bot _ _
+
+variable [StrongRankCondition R]
+
+public lemma index_of_surjective (hf : Surjective f) :
+    f.index = finrank R f.ker := by
+  rw [index_eq_finrank_sub, range_eq_top.mpr hf]
+  simp [finrank_eq_zero_of_subsingleton]
+
+@[simp] public lemma index_id :
+    (id : M →ₗ[R] M).index = 0 := by
+  nontriviality R
+  rw [index_eq_finrank_sub, range_id]
+  simp [finrank_eq_zero_of_subsingleton]
+
+@[simp] public lemma _root_.LinearEquiv.index_eq_zero {e : M ≃ₗ[R] N} :
+    e.toLinearMap.index = 0 := by
+  nontriviality R
+  have := index_of_injective e.injective
+  have := index_of_surjective e.surjective
+  lia
+
+end Ring
+
+section DivisionRing
+
+variable {k : Type*} [DivisionRing k] [Module k M] [Module k N] {f : M →ₗ[k] N}
+
+@[simp] public lemma index_neg :
+    (-f).index = f.index := by
+  rw [index_eq_finrank_sub, index_eq_finrank_sub, ker_neg, range_neg]
+
+public lemma index_eq_of_finiteDimensional [FiniteDimensional k M] [FiniteDimensional k N] :
+    f.index = finrank k M - finrank k N := by
+  -- `0 → f.ker → M → N → f.coker → 0`
+  rw [index_eq_finrank_sub]
+  have h₁ := f.range.finrank_quotient_add_finrank
+  have h₂ := f.quotKerEquivRange.finrank_eq
+  have h₃ := f.ker.finrank_quotient_add_finrank
+  lia
+
+open Submodule in
+@[simp] public lemma index_comp {P : Type*} [AddCommGroup P] [Module k P] (g : N →ₗ[k] P)
+    [FiniteDimensional k f.ker] [FiniteDimensional k g.ker]
+    [FiniteDimensional k (N ⧸ f.range)] [FiniteDimensional k (P ⧸ g.range)] :
+    (g ∘ₗ f).index = g.index + f.index := by
+  -- `0 → f.ker → (g ∘ₗ f).ker → g.ker → f.coker → (g ∘ₗ f).coker → g.coker → 0`
+  have aux : f.range ≤ comap g (g ∘ₗ f).range := by rw [← map_le_iff_le_comap, range_comp]
+  let f₀ : f.ker →ₗ[k] (g ∘ₗ f).ker := inclusion <| ker_le_ker_comp f g
+  let f₁ : (g ∘ₗ f).ker →ₗ[k] g.ker := f.restrict <| by simp
+  let f₂ : g.ker →ₗ[k] N ⧸ f.range := f.range.mkQ ∘ₗ g.ker.subtype
+  let f₃ : (N ⧸ f.range) →ₗ[k] P ⧸ (g ∘ₗ f).range := f.range.mapQ (g ∘ₗ f).range g aux
+  let f₄ : (P ⧸ (g ∘ₗ f).range) →ₗ[k] P ⧸ g.range := factor <| range_comp_le_range f g
+  have h₀ : Injective f₀ := inclusion_injective _
+  have h₁ : Exact f₀ f₁ := by rw [exact_iff]; simp [f₀, f₁, ker_restrict, range_inclusion]
+  have h₂ : Exact f₁ f₂ := by rw [exact_iff]; simp [f₁, f₂, ker_comp, map_comap_eq]
+  have h₃ : Exact f₂ f₃ := by rw [exact_iff]; simp [f₂, f₃, range_comp, ker_mapQ, comap_map_eq]
+  have h₄ : Exact f₃ f₄ := by rw [exact_iff]; simp [f₃, f₄, factor, ker_mapQ, range_mapQ]
+  have h₅ : Surjective f₄ := factor_surjective _
+  have : FiniteDimensional k (g ∘ₗ f).ker := by rw [ker_comp]; infer_instance
+  have : FiniteDimensional k (P ⧸ (g ∘ₗ f).range) := by rw [range_comp]; infer_instance
+  grind [index, sum_neg_one_pow_finrank_eq_zero_of_exact_six f₀ f₁ f₂ f₃ f₄ h₀ h₁ h₂ h₃ h₄ h₅]
+
+end DivisionRing
+
+section Field
+
+variable {k : Type*} [Field k] [Module k M] [Module k N] {f : M →ₗ[k] N}
+
+public lemma index_smul (t : k) (ht : t ≠ 0) :
+    (t • f).index = f.index := by
+  rw [index_eq_finrank_sub, index_eq_finrank_sub, ker_smul _ _ ht, range_smul _ _ ht]
+
+end Field
+
+end LinearMap

Mathlib/Algebra/Module/LinearMap/Index.lean

@@ -5,7 +5,7 @@ Authors: Andrew Yang, Jujian Zhang
 -/
 module
 
-public import Mathlib.Algebra.Exact
+public import Mathlib.Algebra.Exact.Basic
 public import Mathlib.Algebra.Module.LocalizedModule.Basic
 
 /-!