Bases of the middle term of a short exact sequence, with arbitrary lifts

Let 0 → A → B → C → 0 be a short exact sequence of modules, given by an injective linear map f : A →ₗ[R] B and a linear map g : B →ₗ[R] C with Function.Exact f g. A basis a of A, a basis c of C and any family s of lifts of c through g combine into the basis Module.Basis.ofExactLift of B, indexed by the sum of the two index types: it is f ∘ a on the left summand and s on the right summand.

Unlike Mathlib's ModuleCat.Basis.ofShortExact and Module.Basis.sumQuot, which fix one choice of lifts, the lifts here are arbitrary. This is what the bracket determinants [a s / b] of Reidemeister torsion need: in a short exact sequence, the determinant of ofExactLift a c s with respect to a basis of B changes by a.det a' * c.det c' when a, c are replaced by a', c', and does not depend on the lifts at all (Module.Basis.det_ofExactLift), because the transition matrix between two such bases is block upper triangular (Module.Basis.toMatrix_ofExactLift).

Main declarations

• Module.Basis.ofExactLift: the basis of B assembled from a, c and the lifts s.
• Module.Basis.eq_ofExactLift: every basis of B made of the image of a followed by lifts of c is of this form.
• Module.Basis.eq_reindex_ofExactLift: the same for a basis indexed by Fin (m + n).
• Module.Basis.coe_reindex_ofExactLift: indexed by Fin (m + n), the basis ofExactLift is Fin.append (f ∘ a) s.
• Module.Basis.exists_coe_eq_append_lift: for surjective g, some lifts s of c give such a basis Fin.append (f ∘ a) s.
• Module.Basis.ofExactLift_det_eq_mul: the determinant with respect to such a basis of a family made of images of a family x of A and of lifts of a family y of C is a.det x * c.det y.
• Module.Basis.ofExactLift_det_ofExactLift: the determinant of one such basis with respect to another is a.det a' * c.det c'.
• Module.Basis.det_ofExactLift: the corresponding transformation law for the determinant with respect to an arbitrary basis of B.

References

• J. Milnor, Whitehead torsion, Bull. Amer. Math. Soc. 72 (1966), §3.
• V. Turaev, Introduction to combinatorial torsions, Birkhäuser 2001, §1.

noncomputable def Module.Basis.ofExactLift {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Semiring R] [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module R A] [Module R B] [Module R C] {f : A →ₗ[R] B} {g : B →ₗ[R] C} {κ : Type u_5} {σ : Type u_6} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) (a : Basis κ R A) (c : Basis σ R C) (s : σ → B) (hs : ∀ (j : σ), g (s j) = c j) : Basis (κ ⊕ σ) R B

In a short exact sequence 0 → A → B → C → 0, a basis a of A, a basis c of C and lifts s of the vectors of c through B → C together form a basis of B, indexed by κ ⊕ σ: the image of a on the left summand and the lifts s on the right summand.

@[simp]

theorem Module.Basis.ofExactLift_inl {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Semiring R] [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module R A] [Module R B] [Module R C] {f : A →ₗ[R] B} {g : B →ₗ[R] C} {κ : Type u_5} {σ : Type u_6} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) (a : Basis κ R A) (c : Basis σ R C) (s : σ → B) (hs : ∀ (j : σ), g (s j) = c j) (i : κ) : (ofExactLift hf hfg a c s hs) (Sum.inl i) = f (a i)

On the left summand, ofExactLift is the image of the basis a of A.

@[simp]

theorem Module.Basis.ofExactLift_inr {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Semiring R] [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module R A] [Module R B] [Module R C] {f : A →ₗ[R] B} {g : B →ₗ[R] C} {κ : Type u_5} {σ : Type u_6} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) (a : Basis κ R A) (c : Basis σ R C) (s : σ → B) (hs : ∀ (j : σ), g (s j) = c j) (j : σ) : (ofExactLift hf hfg a c s hs) (Sum.inr j) = s j

On the right summand, ofExactLift is the chosen family s of lifts.

@[simp]

theorem Module.Basis.ofExactLift_repr_inr {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Semiring R] [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module R A] [Module R B] [Module R C] {f : A →ₗ[R] B} {g : B →ₗ[R] C} {κ : Type u_5} {σ : Type u_6} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) (a : Basis κ R A) (c : Basis σ R C) (s : σ → B) (hs : ∀ (j : σ), g (s j) = c j) (y : B) (j : σ) : ((ofExactLift hf hfg a c s hs).repr y) (Sum.inr j) = (c.repr (g y)) j

The coordinates of a vector of B on the right summand of ofExactLift are the coordinates of its image in C.

@[simp]

theorem Module.Basis.ofExactLift_repr_apply_inl {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Semiring R] [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module R A] [Module R B] [Module R C] {f : A →ₗ[R] B} {g : B →ₗ[R] C} {κ : Type u_5} {σ : Type u_6} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) (a : Basis κ R A) (c : Basis σ R C) (s : σ → B) (hs : ∀ (j : σ), g (s j) = c j) (x : A) (i : κ) : ((ofExactLift hf hfg a c s hs).repr (f x)) (Sum.inl i) = (a.repr x) i

The coordinates of a vector of A, viewed in B, on the left summand of ofExactLift are its coordinates in a.

theorem Module.Basis.eq_ofExactLift {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Semiring R] [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module R A] [Module R B] [Module R C] {f : A →ₗ[R] B} {g : B →ₗ[R] C} {κ : Type u_5} {σ : Type u_6} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) (a : Basis κ R A) (c : Basis σ R C) (b : Basis (κ ⊕ σ) R B) (hb : ∀ (i : κ), b (Sum.inl i) = f (a i)) (hb' : ∀ (j : σ), g (b (Sum.inr j)) = c j) : b = ofExactLift hf hfg a c (fun (j : σ) => b (Sum.inr j)) hb'

A basis of B indexed by κ ⊕ σ that is the image of the basis a of A on the left summand, and whose vectors on the right summand lift the basis c of C, is the basis ofExactLift with these lifts.

theorem Module.Basis.eq_reindex_ofExactLift {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Semiring R] [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module R A] [Module R B] [Module R C] {f : A →ₗ[R] B} {g : B →ₗ[R] C} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) {m n : ℕ} (a : Basis (Fin m) R A) (c : Basis (Fin n) R C) (b : Basis (Fin (m + n)) R B) (hb : ∀ (i : Fin m), b (Fin.castAdd n i) = f (a i)) (hb' : ∀ (j : Fin n), g (b (Fin.natAdd m j)) = c j) : b = (ofExactLift hf hfg a c (fun (j : Fin n) => b (Fin.natAdd m j)) hb').reindex finSumFinEquiv

A basis of B indexed by Fin (m + n) that is the image of the basis a of A on the first m indices, and whose last n vectors lift the basis c of C, is the basis ofExactLift with these lifts, reindexed by finSumFinEquiv.

theorem Module.Basis.coe_reindex_ofExactLift {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Semiring R] [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module R A] [Module R B] [Module R C] {f : A →ₗ[R] B} {g : B →ₗ[R] C} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) {m n : ℕ} (a : Basis (Fin m) R A) (c : Basis (Fin n) R C) (s : Fin n → B) (hs : ∀ (j : Fin n), g (s j) = c j) : ⇑((ofExactLift hf hfg a c s hs).reindex finSumFinEquiv) = Fin.append (⇑f ∘ ⇑a) s

Reindexed by finSumFinEquiv, the basis ofExactLift lists the image of the basis a of A followed by the lifts s.

theorem Module.Basis.exists_coe_eq_append_lift {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Semiring R] [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module R A] [Module R B] [Module R C] {f : A →ₗ[R] B} {g : B →ₗ[R] C} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) {m n : ℕ} (a : Basis (Fin m) R A) (c : Basis (Fin n) R C) : ∃ (s : Fin n → B) (b : Basis (Fin (m + n)) R B), ⇑g ∘ s = ⇑c ∧ ⇑b = Fin.append (⇑f ∘ ⇑a) s

In a short exact sequence 0 → A → B → C → 0, a basis a of A and a basis c of C indexed by Fin m and Fin n give lifts s of c and a basis of B indexed by Fin (m + n) that lists the image of a followed by s.

theorem Module.Basis.toMatrix_ofExactLift {R : Type u_7} {A : Type u_8} {B : Type u_9} {C : Type u_10} [CommSemiring R] [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module R A] [Module R B] [Module R C] {f : A →ₗ[R] B} {g : B →ₗ[R] C} {κ : Type u_11} {σ : Type u_12} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) (a : Basis κ R A) (c : Basis σ R C) (s : σ → B) (hs : ∀ (j : σ), g (s j) = c j) {κ' : Type u_13} {σ' : Type u_14} (x : κ' → A) (y : σ' → C) (v : κ' ⊕ σ' → B) (hx : ∀ (i : κ'), v (Sum.inl i) = f (x i)) (hy : ∀ (j : σ'), g (v (Sum.inr j)) = y j) : (ofExactLift hf hfg a c s hs).toMatrix v = Matrix.fromBlocks (a.toMatrix x) (Matrix.of fun (i : κ) (j : σ') => ((ofExactLift hf hfg a c s hs).repr (v (Sum.inr j))) (Sum.inl i)) 0 (c.toMatrix y)

The matrix with respect to ofExactLift a c s of a family v of B, made of the images of a family x of A followed by lifts of a family y of C, is block upper triangular, with diagonal blocks the matrices of x with respect to a and of y with respect to c.

theorem Module.Basis.ofExactLift_det_eq_mul {R : Type u_7} {A : Type u_8} {B : Type u_9} {C : Type u_10} [CommRing R] [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module R A] [Module R B] [Module R C] {f : A →ₗ[R] B} {g : B →ₗ[R] C} {κ : Type u_11} {σ : Type u_12} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) (a : Basis κ R A) (c : Basis σ R C) (s : σ → B) (hs : ∀ (j : σ), g (s j) = c j) [Fintype κ] [Fintype σ] [DecidableEq κ] [DecidableEq σ] (x : κ → A) (y : σ → C) (v : κ ⊕ σ → B) (hx : ∀ (i : κ), v (Sum.inl i) = f (x i)) (hy : ∀ (j : σ), g (v (Sum.inr j)) = y j) : (ofExactLift hf hfg a c s hs).det v = a.det x * c.det y

The determinant with respect to ofExactLift a c s of a family v of B, made of the images of a family x of A followed by lifts of a family y of C, is a.det x * c.det y: the matrix of v is block upper triangular.

theorem Module.Basis.ofExactLift_det_ofExactLift {R : Type u_7} {A : Type u_8} {B : Type u_9} {C : Type u_10} [CommRing R] [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module R A] [Module R B] [Module R C] {f : A →ₗ[R] B} {g : B →ₗ[R] C} {κ : Type u_11} {σ : Type u_12} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) (a a' : Basis κ R A) (c c' : Basis σ R C) (s s' : σ → B) (hs : ∀ (j : σ), g (s j) = c j) (hs' : ∀ (j : σ), g (s' j) = c' j) [Fintype κ] [Fintype σ] [DecidableEq κ] [DecidableEq σ] : (ofExactLift hf hfg a c s hs).det ⇑(ofExactLift hf hfg a' c' s' hs') = a.det ⇑a' * c.det ⇑c'

The determinant of one basis of the form ofExactLift with respect to another is the product of the determinants of the bases of A and of C; in particular it does not depend on the lifts.

theorem Module.Basis.det_ofExactLift {R : Type u_7} {A : Type u_8} {B : Type u_9} {C : Type u_10} [CommRing R] [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module R A] [Module R B] [Module R C] {f : A →ₗ[R] B} {g : B →ₗ[R] C} {κ : Type u_11} {σ : Type u_12} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) (a a' : Basis κ R A) (c c' : Basis σ R C) (s s' : σ → B) (hs : ∀ (j : σ), g (s j) = c j) (hs' : ∀ (j : σ), g (s' j) = c' j) [Fintype κ] [Fintype σ] [DecidableEq κ] [DecidableEq σ] (b : Basis (κ ⊕ σ) R B) : b.det ⇑(ofExactLift hf hfg a' c' s' hs') = b.det ⇑(ofExactLift hf hfg a c s hs) * (a.det ⇑a' * c.det ⇑c')

Replacing the bases a, c and the lifts s in ofExactLift multiplies its determinant with respect to any basis b of B by a.det a' * c.det c'. In particular the determinant does not depend on the choice of lifts.