Schanuel's lemma for projective presentations

Schanuel's lemma compares two surjections π : P → M and ρ : Q → M from projective modules: their kernels agree after adding Q and P. This file proves it in the stronger automorphism form that also records the maps: π ∘ fst and ρ ∘ snd are two maps P × Q → M which differ by an automorphism of P × Q. The argument is that of Schanuel's lemma — lift each map through the other and shear — and it needs no surjectivity, only that the two maps have the same range (TauCeti.exists_linearEquiv_comp_fst_eq_comp_snd_comp).

The second shear follows the shear argument in the proof of Submodule.minorsIdeal_ker_eq_prod_top in TauCeti/RingTheory/FittingIdeal/Basic.lean.

Applied twice, once to the surjections P₀ → M and Q₀ → M and once to the first maps of two projective presentations P₁ → P₀ → M → 0 and Q₁ → Q₀ → M → 0, it shows that any two projective presentations of the same module become isomorphic as arrows once each is enlarged by the identity of the other's middle term and by a zero map out of the remaining projectives (TauCeti.exists_linearEquiv_comp_prodMap_comp_fst_eq). This is what makes a construction from a projective presentation that is additive in the arrow — the Auslander–Bridger transpose, for instance — independent of the presentation up to summands built from projectives.

Main results

• TauCeti.exists_comp_eq_of_range_le: a map from a projective module factors through any map whose range contains its range.
• TauCeti.exists_lift_projective_presentation: module maps lift to commutative squares between projective presentations.
• TauCeti.exists_linearEquiv_comp_fst_eq_comp_snd_comp: two maps from projective modules with equal ranges differ, after stabilisation, by an automorphism.
• TauCeti.exists_linearEquiv_comp_prodMap_comp_fst_eq: two projective presentations of the same module are stably isomorphic as arrows.

References

• M. Auslander, M. Bridger, Stable module theory, Mem. Amer. Math. Soc. 94 (1969), Section 2.1.
• T. Y. Lam, Lectures on Modules and Rings, Graduate Texts in Mathematics 189, Springer (1999), (5.1) (Schanuel's lemma).

theorem TauCeti.exists_comp_eq_of_range_le {R : Type u_1} [Semiring R] {A : Type u_2} {B : Type u_3} {E : Type u_4} [AddCommMonoid E] [Module R E] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [Module.Projective R A] {a : A →ₗ[R] E} {b : B →ₗ[R] E} (h : a.range ≤ b.range) : ∃ (α : A →ₗ[R] B), b ∘ₗ α = a

A map from a projective module factors through any map whose range contains its range. This is the lifting property of projective modules, applied to the corestriction onto the range.

theorem TauCeti.exists_linearEquiv_comp_fst_eq_comp_snd_comp {R : Type u_1} [Semiring R] {A : Type u_2} {B : Type u_3} {E : Type u_4} [AddCommMonoid E] [Module R E] [AddCommGroup A] [Module R A] [AddCommGroup B] [Module R B] [Module.Projective R A] [Module.Projective R B] {a : A →ₗ[R] E} {b : B →ₗ[R] E} (h : a.range = b.range) : ∃ (e : (A × B) ≃ₗ[R] A × B), a ∘ₗ LinearMap.fst R A B = b ∘ₗ LinearMap.snd R A B ∘ₗ ↑e

Schanuel's lemma in automorphism form. If a : A → E and b : B → E are maps from projective modules with the same range, then a ∘ fst and b ∘ snd, as maps A × B → E, differ by an automorphism of A × B.

For surjective a and b this is Schanuel's lemma: the automorphism carries ker (a ∘ fst) = ker a × B onto ker (b ∘ snd) = A × ker b.

theorem TauCeti.exists_lift_projective_presentation {R : Type u_1} [Semiring R] {M : Type u_2} {N : Type u_3} {P₀ : Type u_4} {P₁ : Type u_5} {Q₀ : Type u_6} {Q₁ : Type u_7} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P₀] [Module R P₀] [AddCommMonoid P₁] [Module R P₁] [AddCommMonoid Q₀] [Module R Q₀] [AddCommMonoid Q₁] [Module R Q₁] {p : P₁ →ₗ[R] P₀} {q : Q₁ →ₗ[R] Q₀} {π : P₀ →ₗ[R] M} {ρ : Q₀ →ₗ[R] N} [Module.Projective R P₀] [Module.Projective R P₁] (hp : π ∘ₗ p = 0) (hq : Function.Exact ⇑q ⇑ρ) (hρ : Function.Surjective ⇑ρ) (f : M →ₗ[R] N) : ∃ (f₀ : P₀ →ₗ[R] Q₀) (f₁ : P₁ →ₗ[R] Q₁), ρ ∘ₗ f₀ = f ∘ₗ π ∧ f₀ ∘ₗ p = q ∘ₗ f₁

A map to a presented module lifts to a square from any complex with projective terms. In particular, module maps lift to squares between projective presentations. The source needs only a zero composite, and the target needs exactness and a surjective augmentation.

theorem TauCeti.exists_linearEquiv_comp_prodMap_comp_fst_eq {R : Type u_1} [Semiring R] {M : Type u_2} {P₀ : Type u_3} {P₁ : Type u_4} {Q₀ : Type u_5} {Q₁ : Type u_6} [AddCommMonoid M] [Module R M] [AddCommGroup P₀] [Module R P₀] [AddCommGroup P₁] [Module R P₁] [AddCommGroup Q₀] [Module R Q₀] [AddCommGroup Q₁] [Module R Q₁] [Module.Projective R P₀] [Module.Projective R P₁] [Module.Projective R Q₀] [Module.Projective R Q₁] {f : P₁ →ₗ[R] P₀} {π : P₀ →ₗ[R] M} {g : Q₁ →ₗ[R] Q₀} {ρ : Q₀ →ₗ[R] M} (hf : Function.Exact ⇑f ⇑π) (hπ : Function.Surjective ⇑π) (hg : Function.Exact ⇑g ⇑ρ) (hρ : Function.Surjective ⇑ρ) : ∃ (e₀ : (P₀ × Q₀) ≃ₗ[R] P₀ × Q₀) (e₁ : ((P₁ × Q₀) × P₀ × Q₁) ≃ₗ[R] (P₁ × Q₀) × P₀ × Q₁), ↑e₀ ∘ₗ f.prodMap LinearMap.id ∘ₗ LinearMap.fst R (P₁ × Q₀) (P₀ × Q₁) = LinearMap.id.prodMap g ∘ₗ LinearMap.snd R (P₁ × Q₀) (P₀ × Q₁) ∘ₗ ↑e₁

Two projective presentations are stably isomorphic arrows. Let P₁ → P₀ → M → 0 and Q₁ → Q₀ → M → 0 be projective presentations of the same module, with first maps f and g. Enlarge f to (f ⊕ id_{Q₀}) ∘ fst : (P₁ × Q₀) × (P₀ × Q₁) → P₀ × Q₀ and g to (id_{P₀} ⊕ g) ∘ snd, on the same source and target. These two arrows are isomorphic: there are automorphisms e₀ of the target and e₁ of the source with e₀ ∘ (f ⊕ id) ∘ fst = (id ⊕ g) ∘ snd ∘ e₁.

The presentations need not be finite, and the presented module is arbitrary.