The six-term sequence of lim and lim¹

Let 0 → A → B → C → 0 be a sequence of towers of R-modules, given by morphisms of towers f : A ⟶ B and g : B ⟶ C which are exact at every level, with fₙ injective and gₙ surjective. Then the products of the terms form a short exact sequence commuting with the shift maps, and the snake lemma gives an exact sequence

0 → lim A → lim B → lim C → lim¹ A → lim¹ B → lim¹ C → 0.

This file constructs the connecting map ModuleTower.connecting : lim C → lim¹ A, characterizes it by ModuleTower.connecting_apply (lift a compatible family c to a family b of B; its shift comes from a family a of A, and the connecting map sends c to the class of a), proves exactness at each of the six terms and the naturality of the connecting map in morphisms of short exact sequences of towers. Each exactness statement only assumes the levelwise injectivity, exactness and surjectivity it uses. As a consequence, lim B → lim C is surjective whenever lim¹ A vanishes, for instance when the transitions of A are surjective (ModuleTower.subsingleton_limOne_of_surjective).

This six-term sequence is the input to Milnor sequences for towers of complexes and to the long exact sequences of derived limits of towers.

Main declarations

• TauCeti.ModuleTower.connecting: the connecting map lim C → lim¹ A.
• TauCeti.ModuleTower.exact_limMap, TauCeti.ModuleTower.exact_limMap_connecting, TauCeti.ModuleTower.exact_connecting_limOneMap, TauCeti.ModuleTower.exact_limOneMap: exactness of the six-term sequence; exactness at the two ends is TauCeti.ModuleTower.limMap_injective and TauCeti.ModuleTower.limOneMap_surjective.
• TauCeti.ModuleTower.connecting_naturality: naturality of the connecting map.
• TauCeti.ModuleTower.exact_lim_subtype_shift: lim A ↪ ∏ₙ Aₙ → ∏ₙ Aₙ is exact, the input to the short exact sequence of a tower of complexes.
• TauCeti.ModuleTower.limMap_surjective_of_subsingleton_limOne: lim B → lim C is surjective when lim¹ A = 0.

References

• Stacks: More on Algebra, Lemma 15.88.1, Tag 07KW
• Stacks: Algebra, Lemma 10.86.4, Tag 0598
• C. A. Weibel, An introduction to homological algebra, §3.5.

theorem TauCeti.ModuleTower.exact_productMap {R : Type u} [Ring R] {F G H : ModuleTower R} {f : F ⟶ G} {g : G ⟶ H} (hfg : ∀ (n : ℕ), Function.Exact ⇑(ModuleCat.Hom.hom (f.app (Opposite.op n))) ⇑(ModuleCat.Hom.hom (g.app (Opposite.op n)))) : Function.Exact ⇑(productMap f) ⇑(productMap g)

A levelwise exact pair of morphisms of towers is exact on products.

theorem TauCeti.ModuleTower.comp_eq_zero_of_exact {R : Type u} [Ring R] {F G H : ModuleTower R} {f : F ⟶ G} {g : G ⟶ H} (hfg : ∀ (n : ℕ), Function.Exact ⇑(ModuleCat.Hom.hom (f.app (Opposite.op n))) ⇑(ModuleCat.Hom.hom (g.app (Opposite.op n)))) : CategoryTheory.CategoryStruct.comp f g = 0

A levelwise exact pair of morphisms of towers composes to zero.

theorem TauCeti.ModuleTower.exact_limMap {R : Type u} [Ring R] {F G H : ModuleTower R} {f : F ⟶ G} {g : G ⟶ H} (hf : ∀ (n : ℕ), Function.Injective ⇑(ModuleCat.Hom.hom (f.app (Opposite.op n)))) (hfg : ∀ (n : ℕ), Function.Exact ⇑(ModuleCat.Hom.hom (f.app (Opposite.op n))) ⇑(ModuleCat.Hom.hom (g.app (Opposite.op n)))) : Function.Exact ⇑(limMap f) ⇑(limMap g)

Exactness of lim A → lim B → lim C for a levelwise exact sequence 0 → A → B → C.

theorem TauCeti.ModuleTower.limMap_surjective_of_subsingleton_limOne {R : Type u} [Ring R] {F G H : ModuleTower R} {f : F ⟶ G} {g : G ⟶ H} (hfg : ∀ (n : ℕ), Function.Exact ⇑(ModuleCat.Hom.hom (f.app (Opposite.op n))) ⇑(ModuleCat.Hom.hom (g.app (Opposite.op n)))) (hg : ∀ (n : ℕ), Function.Surjective ⇑(ModuleCat.Hom.hom (g.app (Opposite.op n)))) [Subsingleton F.limOne] : Function.Surjective ⇑(limMap g)

If lim¹ A vanishes, then for a levelwise exact sequence A → B → C → 0 the map lim B → lim C is surjective.

theorem TauCeti.ModuleTower.exact_limOneMap {R : Type u} [Ring R] {F G H : ModuleTower R} {f : F ⟶ G} {g : G ⟶ H} (hfg : ∀ (n : ℕ), Function.Exact ⇑(ModuleCat.Hom.hom (f.app (Opposite.op n))) ⇑(ModuleCat.Hom.hom (g.app (Opposite.op n)))) (hg : ∀ (n : ℕ), Function.Surjective ⇑(ModuleCat.Hom.hom (g.app (Opposite.op n)))) : Function.Exact ⇑(limOneMap f) ⇑(limOneMap g)

Exactness of lim¹ A → lim¹ B → lim¹ C for a levelwise exact sequence A → B → C → 0.

theorem TauCeti.ModuleTower.exact_lim_subtype_shift {R : Type u} [Ring R] (F : ModuleTower R) : Function.Exact ⇑F.lim.subtype ⇑F.shift

lim A ↪ ∏ₙ Aₙ → ∏ₙ Aₙ is exact: lim A is the kernel of the shift.

noncomputable def TauCeti.ModuleTower.connecting {R : Type u} [Ring R] {F G H : ModuleTower R} (f : F ⟶ G) (g : G ⟶ H) (hf : ∀ (n : ℕ), Function.Injective ⇑(ModuleCat.Hom.hom (f.app (Opposite.op n)))) (hfg : ∀ (n : ℕ), Function.Exact ⇑(ModuleCat.Hom.hom (f.app (Opposite.op n))) ⇑(ModuleCat.Hom.hom (g.app (Opposite.op n)))) (hg : ∀ (n : ℕ), Function.Surjective ⇑(ModuleCat.Hom.hom (g.app (Opposite.op n)))) : ↥H.lim →ₗ[R] F.limOne

The connecting map lim C → lim¹ A of the six-term sequence of a levelwise short exact sequence of towers 0 → A → B → C → 0. It sends a compatible family c to the class of any family a of A with f(a) = δ(b) for some lift b of c; see connecting_apply.

theorem TauCeti.ModuleTower.connecting_apply {R : Type u} [Ring R] {F G H : ModuleTower R} (f : F ⟶ G) (g : G ⟶ H) (hf : ∀ (n : ℕ), Function.Injective ⇑(ModuleCat.Hom.hom (f.app (Opposite.op n)))) (hfg : ∀ (n : ℕ), Function.Exact ⇑(ModuleCat.Hom.hom (f.app (Opposite.op n))) ⇑(ModuleCat.Hom.hom (g.app (Opposite.op n)))) (hg : ∀ (n : ℕ), Function.Surjective ⇑(ModuleCat.Hom.hom (g.app (Opposite.op n)))) (c : ↥H.lim) (b : G.Product) (hb : (productMap g) b = ↑c) (a : F.Product) (ha : (productMap f) a = G.shift b) : (connecting f g hf hfg hg) c = Submodule.Quotient.mk a

The connecting map of the six-term sequence. If b lifts the compatible family c of C and f(a) = δ(b), then c is sent to the class of a in lim¹ A.

theorem TauCeti.ModuleTower.exact_limMap_connecting {R : Type u} [Ring R] {F G H : ModuleTower R} (f : F ⟶ G) (g : G ⟶ H) (hf : ∀ (n : ℕ), Function.Injective ⇑(ModuleCat.Hom.hom (f.app (Opposite.op n)))) (hfg : ∀ (n : ℕ), Function.Exact ⇑(ModuleCat.Hom.hom (f.app (Opposite.op n))) ⇑(ModuleCat.Hom.hom (g.app (Opposite.op n)))) (hg : ∀ (n : ℕ), Function.Surjective ⇑(ModuleCat.Hom.hom (g.app (Opposite.op n)))) : Function.Exact ⇑(limMap g) ⇑(connecting f g hf hfg hg)

Exactness of lim B → lim C → lim¹ A.

theorem TauCeti.ModuleTower.exact_connecting_limOneMap {R : Type u} [Ring R] {F G H : ModuleTower R} (f : F ⟶ G) (g : G ⟶ H) (hf : ∀ (n : ℕ), Function.Injective ⇑(ModuleCat.Hom.hom (f.app (Opposite.op n)))) (hfg : ∀ (n : ℕ), Function.Exact ⇑(ModuleCat.Hom.hom (f.app (Opposite.op n))) ⇑(ModuleCat.Hom.hom (g.app (Opposite.op n)))) (hg : ∀ (n : ℕ), Function.Surjective ⇑(ModuleCat.Hom.hom (g.app (Opposite.op n)))) : Function.Exact ⇑(connecting f g hf hfg hg) ⇑(limOneMap f)

Exactness of lim C → lim¹ A → lim¹ B.

theorem TauCeti.ModuleTower.connecting_naturality {R : Type u} [Ring R] {F G H : ModuleTower R} (f : F ⟶ G) (g : G ⟶ H) (hf : ∀ (n : ℕ), Function.Injective ⇑(ModuleCat.Hom.hom (f.app (Opposite.op n)))) (hfg : ∀ (n : ℕ), Function.Exact ⇑(ModuleCat.Hom.hom (f.app (Opposite.op n))) ⇑(ModuleCat.Hom.hom (g.app (Opposite.op n)))) (hg : ∀ (n : ℕ), Function.Surjective ⇑(ModuleCat.Hom.hom (g.app (Opposite.op n)))) {F' G' H' : ModuleTower R} {f' : F' ⟶ G'} {g' : G' ⟶ H'} (hf' : ∀ (n : ℕ), Function.Injective ⇑(ModuleCat.Hom.hom (f'.app (Opposite.op n)))) (hfg' : ∀ (n : ℕ), Function.Exact ⇑(ModuleCat.Hom.hom (f'.app (Opposite.op n))) ⇑(ModuleCat.Hom.hom (g'.app (Opposite.op n)))) (hg' : ∀ (n : ℕ), Function.Surjective ⇑(ModuleCat.Hom.hom (g'.app (Opposite.op n)))) (α : F ⟶ F') (β : G ⟶ G') (γ : H ⟶ H') (h₁ : CategoryTheory.CategoryStruct.comp f β = CategoryTheory.CategoryStruct.comp α f') (h₂ : CategoryTheory.CategoryStruct.comp g γ = CategoryTheory.CategoryStruct.comp β g') : limOneMap α ∘ₗ connecting f g hf hfg hg = connecting f' g' hf' hfg' hg' ∘ₗ limMap γ

Naturality of the connecting map. A morphism (α, β, γ) from the short exact sequence of towers 0 → A → B → C → 0 to 0 → A' → B' → C' → 0 gives a commutative square relating the two connecting maps lim C → lim¹ A and lim C' → lim¹ A'.