lim and lim¹ of towers of modules

A tower of modules over a ring R is a functor ℕᵒᵖ ⥤ ModuleCat R, that is, a sequence of modules A₀ ← A₁ ← A₂ ← ⋯ with transition maps φₙ : Aₙ₊₁ → Aₙ. On the product ∏ₙ Aₙ the shift δ(x)ₙ = xₙ - φₙ(xₙ₊₁) is R-linear; its kernel lim A is the module of compatible families and its cokernel is lim¹ A. This file shows that lim A, with its projections, is a limit of the tower in ModuleCat R, that lim¹ A vanishes if and only if the shift is surjective, and hence that lim¹ A vanishes when every transition map is surjective. By Stacks, Tag 07KW, lim and lim¹ are the derived functors R⁰lim and R¹lim on ℕ-indexed towers, whose higher derived limits vanish; that identification is not formalized here. The shift presentation is the input to the six-term sequence of a short exact sequence of towers, to Milnor sequences for towers of complexes, and to derived limits of towers of modules.

The ring R is only assumed associative and unital, so towers of left modules over a noncommutative ring are allowed.

Main declarations

• TauCeti.ModuleTower: towers of R-modules, the functor category ℕᵒᵖ ⥤ ModuleCat R.
• TauCeti.ModuleTower.transitionOfLE: the composite transition maps Aₖ → Aₙ, n ≤ k.
• TauCeti.ModuleTower.shift: the shift map δ on the product of the terms.
• TauCeti.ModuleTower.lim, TauCeti.ModuleTower.limOne: its kernel and cokernel.
• TauCeti.ModuleTower.mem_lim: lim consists of the families compatible with the transitions.
• TauCeti.ModuleTower.isLimitLimCone: lim, with its projections, is a limit of the tower.
• TauCeti.ModuleTower.limLift_bijective_of_le: a compatible family of maps into the terms that are bijective from some index on induces a bijection onto lim.
• TauCeti.ModuleTower.limπ_surjective: if the transitions are surjective, so are the projections lim A → Aₙ.
• TauCeti.ModuleTower.isSplitEpi_shift: if the transitions are split epimorphisms, so is the shift map.
• TauCeti.ModuleTower.limMap, TauCeti.ModuleTower.limOneMap: the linear maps induced by a morphism of towers, with their identity, composition, zero and addition laws.
• TauCeti.ModuleTower.limEquivOfIso, TauCeti.ModuleTower.limOneEquivOfIso: the linear equivalences on lim and lim¹ induced by an isomorphism of towers.
• TauCeti.ModuleTower.limMap_inj: a morphism out of a tower with surjective transitions is determined by the map it induces on lim.
• TauCeti.ModuleTower.limMap_injective, TauCeti.ModuleTower.limOneMap_surjective: levelwise injective (surjective) morphisms induce injective (surjective) maps on lim (lim¹).
• TauCeti.ModuleTower.subsingleton_limOne_iff: lim¹ vanishes if and only if the shift map is surjective.
• TauCeti.ModuleTower.mem_range_shift_of_le_map: a family of submodules Bₙ ⊆ φₙ(Bₙ₊₁) has ∏ₙ Bₙ inside the image of the shift map.
• TauCeti.ModuleTower.subsingleton_limOne_of_surjective: towers with surjective transitions have vanishing lim¹.
• TauCeti.ModuleTower.smulTower: the tower M ←f M ←f ⋯ of a module over a commutative ring, whose transitions are multiplication by f.

References

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

@[reducible, inline]

abbrev TauCeti.ModuleTower (R : Type u) [Ring R] : Type (max v (v + 1) u)

A tower of R-modules: a functor ℕᵒᵖ ⥤ ModuleCat R, given by modules Aₙ and transition maps Aₙ₊₁ → Aₙ. Morphisms of towers are natural transformations.

@[reducible, inline]

abbrev TauCeti.ModuleTower.Product {R : Type u} [Ring R] (F : ModuleTower R) : Type v

The product ∏ₙ Aₙ of the terms of a tower.

def TauCeti.ModuleTower.transition {R : Type u} [Ring R] (F : ModuleTower R) (n : ℕ) : ↑(F.obj (Opposite.op (n + 1))) →ₗ[R] ↑(F.obj (Opposite.op n))

The transition map Aₙ₊₁ → Aₙ of a tower.

theorem TauCeti.ModuleTower.transition_def {R : Type u} [Ring R] (F : ModuleTower R) (n : ℕ) : F.transition n = ModuleCat.Hom.hom (F.map (CategoryTheory.homOfLE ⋯).op)

def TauCeti.ModuleTower.transitionOfLE {R : Type u} [Ring R] (F : ModuleTower R) {n k : ℕ} (h : n ≤ k) : ↑(F.obj (Opposite.op k)) →ₗ[R] ↑(F.obj (Opposite.op n))

The composite transition map Aₖ → Aₙ of a tower, for n ≤ k.

theorem TauCeti.ModuleTower.transitionOfLE_def {R : Type u} [Ring R] (F : ModuleTower R) {n k : ℕ} (h : n ≤ k) : F.transitionOfLE h = ModuleCat.Hom.hom (F.map (CategoryTheory.homOfLE h).op)

@[simp]

theorem TauCeti.ModuleTower.map_hom_eq_transitionOfLE {R : Type u} [Ring R] (F : ModuleTower R) {n k : ℕ} (f : Opposite.op k ⟶ Opposite.op n) : ModuleCat.Hom.hom (F.map f) = F.transitionOfLE ⋯

Every map F.map f : Aₖ → Aₙ of a tower is the composite transition transitionOfLE.

@[simp]

theorem TauCeti.ModuleTower.transitionOfLE_succ {R : Type u} [Ring R] (F : ModuleTower R) (n : ℕ) : F.transitionOfLE ⋯ = F.transition n

@[simp]

theorem TauCeti.ModuleTower.transitionOfLE_refl {R : Type u} [Ring R] (F : ModuleTower R) (n : ℕ) : F.transitionOfLE ⋯ = LinearMap.id

@[simp]

theorem TauCeti.ModuleTower.transitionOfLE_comp_transitionOfLE {R : Type u} [Ring R] (F : ModuleTower R) {m n k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) : F.transitionOfLE hmn ∘ₗ F.transitionOfLE hnk = F.transitionOfLE ⋯

@[simp]

theorem TauCeti.ModuleTower.transitionOfLE_transitionOfLE {R : Type u} [Ring R] (F : ModuleTower R) {m n k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) (x : ↑(F.obj (Opposite.op k))) : (F.transitionOfLE hmn) ((F.transitionOfLE hnk) x) = (F.transitionOfLE ⋯) x

@[simp]

theorem TauCeti.ModuleTower.transition_transitionOfLE {R : Type u} [Ring R] (F : ModuleTower R) {n k : ℕ} (h : n + 1 ≤ k) (x : ↑(F.obj (Opposite.op k))) : (F.transition n) ((F.transitionOfLE h) x) = (F.transitionOfLE ⋯) x

@[simp]

theorem TauCeti.ModuleTower.transitionOfLE_transition {R : Type u} [Ring R] (F : ModuleTower R) {n k : ℕ} (h : n ≤ k) (x : ↑(F.obj (Opposite.op (k + 1)))) : (F.transitionOfLE h) ((F.transition k) x) = (F.transitionOfLE ⋯) x

theorem TauCeti.ModuleTower.range_transitionOfLE_le {R : Type u} [Ring R] (F : ModuleTower R) {m n k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) : (F.transitionOfLE ⋯).range ≤ (F.transitionOfLE hmn).range

The images of the composite transitions into a fixed term Aₙ decrease as the source index grows.

theorem TauCeti.ModuleTower.transitionOfLE_surjective {R : Type u} [Ring R] (F : ModuleTower R) {m k : ℕ} (h : ∀ (n : ℕ), m ≤ n → Function.Surjective ⇑(F.transition n)) (hmk : m ≤ k) : Function.Surjective ⇑(F.transitionOfLE hmk)

If every transition map F.transition n with m ≤ n is surjective, then so is every composite transition Aₖ → Aₘ.

def TauCeti.ModuleTower.shift {R : Type u} [Ring R] (F : ModuleTower R) : F.Product →ₗ[R] F.Product

The shift map δ : ∏ₙ Aₙ → ∏ₙ Aₙ, δ(x)ₙ = xₙ - φₙ(xₙ₊₁).

@[simp]

theorem TauCeti.ModuleTower.shift_apply {R : Type u} [Ring R] (F : ModuleTower R) (x : F.Product) (n : ℕ) : F.shift x n = x n - (F.transition n) (x (n + 1))

def TauCeti.ModuleTower.lim {R : Type u} [Ring R] (F : ModuleTower R) : Submodule R F.Product

The limit lim A of a tower, the kernel of the shift map: the families (xₙ) with φₙ(xₙ₊₁) = xₙ for every n.

@[reducible, inline]

abbrev TauCeti.ModuleTower.limOne {R : Type u} [Ring R] (F : ModuleTower R) : Type v

The first derived limit lim¹ A of a tower, the cokernel of the shift map.

theorem TauCeti.ModuleTower.lim_eq_ker {R : Type u} [Ring R] (F : ModuleTower R) : F.lim = F.shift.ker

@[simp]

theorem TauCeti.ModuleTower.mem_lim {R : Type u} [Ring R] (F : ModuleTower R) {x : F.Product} : x ∈ F.lim ↔ ∀ (n : ℕ), (F.transition n) (x (n + 1)) = x n

x ∈ lim A if and only if φₙ(xₙ₊₁) = xₙ for every n: lim A is exactly the module of compatible families.

def TauCeti.ModuleTower.limπ {R : Type u} [Ring R] (F : ModuleTower R) (n : ℕ) : ↥F.lim →ₗ[R] ↑(F.obj (Opposite.op n))

The projection lim A → Aₙ.

@[simp]

theorem TauCeti.ModuleTower.limπ_apply {R : Type u} [Ring R] (F : ModuleTower R) (n : ℕ) (x : ↥F.lim) : (F.limπ n) x = ↑x n

theorem TauCeti.ModuleTower.lim_ext {R : Type u} [Ring R] (F : ModuleTower R) {x y : ↥F.lim} (h : ∀ (n : ℕ), (F.limπ n) x = (F.limπ n) y) : x = y

Two points of lim A are equal when all their coordinates agree.

theorem TauCeti.ModuleTower.lim_ext_iff {R : Type u} [Ring R] {F : ModuleTower R} {x y : ↥F.lim} : x = y ↔ ∀ (n : ℕ), (F.limπ n) x = (F.limπ n) y

@[simp]

theorem TauCeti.ModuleTower.transition_coe_lim_succ {R : Type u} [Ring R] (F : ModuleTower R) (x : ↥F.lim) (n : ℕ) : (F.transition n) (↑x (n + 1)) = ↑x n

An element of lim A is compatible with the transition Aₙ₊₁ → Aₙ.

@[simp]

theorem TauCeti.ModuleTower.transition_comp_limπ {R : Type u} [Ring R] (F : ModuleTower R) (n : ℕ) : F.transition n ∘ₗ F.limπ (n + 1) = F.limπ n

theorem TauCeti.ModuleTower.lim_hom_ext {R : Type u} [Ring R] (F : ModuleTower R) {P : Type u_1} [AddCommGroup P] [Module R P] {f g : P →ₗ[R] ↥F.lim} (h : ∀ (n : ℕ), F.limπ n ∘ₗ f = F.limπ n ∘ₗ g) : f = g

theorem TauCeti.ModuleTower.lim_hom_ext_iff {R : Type u} [Ring R] {F : ModuleTower R} {P : Type u_1} [AddCommGroup P] [Module R P] {f g : P →ₗ[R] ↥F.lim} : f = g ↔ ∀ (n : ℕ), F.limπ n ∘ₗ f = F.limπ n ∘ₗ g

def TauCeti.ModuleTower.limLift {R : Type u} [Ring R] (F : ModuleTower R) {P : Type u_1} [AddCommGroup P] [Module R P] (f : (n : ℕ) → P →ₗ[R] ↑(F.obj (Opposite.op n))) (hf : ∀ (n : ℕ), F.transition n ∘ₗ f (n + 1) = f n) : P →ₗ[R] ↥F.lim

The universal property of lim A: a family of linear maps P → Aₙ compatible with the transitions factors through lim A.

@[simp]

theorem TauCeti.ModuleTower.coe_limLift_apply {R : Type u} [Ring R] (F : ModuleTower R) {P : Type u_1} [AddCommGroup P] [Module R P] (f : (n : ℕ) → P →ₗ[R] ↑(F.obj (Opposite.op n))) (hf : ∀ (n : ℕ), F.transition n ∘ₗ f (n + 1) = f n) (p : P) (n : ℕ) : ↑((F.limLift f hf) p) n = (f n) p

@[simp]

theorem TauCeti.ModuleTower.limπ_comp_limLift {R : Type u} [Ring R] (F : ModuleTower R) {P : Type u_1} [AddCommGroup P] [Module R P] (f : (n : ℕ) → P →ₗ[R] ↑(F.obj (Opposite.op n))) (hf : ∀ (n : ℕ), F.transition n ∘ₗ f (n + 1) = f n) (n : ℕ) : F.limπ n ∘ₗ F.limLift f hf = f n

@[simp]

theorem TauCeti.ModuleTower.ker_limLift {R : Type u} [Ring R] (F : ModuleTower R) {P : Type u_1} [AddCommGroup P] [Module R P] (f : (n : ℕ) → P →ₗ[R] ↑(F.obj (Opposite.op n))) (hf : ∀ (n : ℕ), F.transition n ∘ₗ f (n + 1) = f n) : (F.limLift f hf).ker = ⨅ (n : ℕ), (f n).ker

The kernel of the map P → lim A induced by a compatible family of maps fₙ : P → Aₙ is the intersection of the kernels of the fₙ.

def TauCeti.ModuleTower.limCone {R : Type u} [Ring R] (F : ModuleTower R) : CategoryTheory.Limits.Cone F

The cone over a tower with vertex lim A and the projections lim A → Aₙ.

@[simp]

theorem TauCeti.ModuleTower.limCone_pt {R : Type u} [Ring R] (F : ModuleTower R) : F.limCone.pt = ↧↥F.lim

@[simp]

theorem TauCeti.ModuleTower.limCone_π_app {R : Type u} [Ring R] (F : ModuleTower R) (n : ℕ) : ModuleCat.Hom.hom (F.limCone.π.app (Opposite.op n)) = F.limπ n

theorem TauCeti.ModuleTower.map_apply_of_mem_lim {R : Type u} [Ring R] (F : ModuleTower R) {x : F.Product} (hx : x ∈ F.lim) {m n : ℕ} (f : Opposite.op n ⟶ Opposite.op m) : (ModuleCat.Hom.hom (F.map f)) (x n) = x m

An element of lim A is compatible with every composite transition Aₙ → Aₘ, m ≤ n.

theorem TauCeti.ModuleTower.transitionOfLE_apply_of_mem_lim {R : Type u} [Ring R] (F : ModuleTower R) {x : F.Product} (hx : x ∈ F.lim) {n k : ℕ} (h : n ≤ k) : (F.transitionOfLE h) (x k) = x n

An element of lim A is compatible with the composite transition Aₖ → Aₙ, n ≤ k.

@[simp]

theorem TauCeti.ModuleTower.transitionOfLE_coe_lim {R : Type u} [Ring R] (F : ModuleTower R) (x : ↥F.lim) {n k : ℕ} (h : n ≤ k) : (F.transitionOfLE h) (↑x k) = ↑x n

An element of lim A is compatible with the composite transition Aₖ → Aₙ, n ≤ k.

@[simp]

theorem TauCeti.ModuleTower.transitionOfLE_comp_limπ {R : Type u} [Ring R] (F : ModuleTower R) {n k : ℕ} (h : n ≤ k) : F.transitionOfLE h ∘ₗ F.limπ k = F.limπ n

theorem TauCeti.ModuleTower.ker_limπ_antitone {R : Type u} [Ring R] (F : ModuleTower R) : Antitone fun (n : ℕ) => (F.limπ n).ker

The kernels of the projections lim A → Aₙ decrease as n grows.

theorem TauCeti.ModuleTower.limLift_bijective_of_le {R : Type u} [Ring R] (F : ModuleTower R) {P : Type u_1} [AddCommGroup P] [Module R P] (f : (n : ℕ) → P →ₗ[R] ↑(F.obj (Opposite.op n))) (hf : ∀ (n : ℕ), F.transition n ∘ₗ f (n + 1) = f n) (N : ℕ) (h : ∀ (n : ℕ), N ≤ n → Function.Bijective ⇑(f n)) : Function.Bijective ⇑(F.limLift f hf)

If a compatible family of linear maps fₙ : P → Aₙ consists of bijections from some index N on, then the induced map P → lim A is bijective.

def TauCeti.ModuleTower.isLimitLimCone {R : Type u} [Ring R] (F : ModuleTower R) : CategoryTheory.Limits.IsLimit F.limCone

lim A, with its projections, is a limit of the tower A in ModuleCat R.

theorem TauCeti.ModuleTower.subsingleton_limOne_iff {R : Type u} [Ring R] (F : ModuleTower R) : Subsingleton F.limOne ↔ Function.Surjective ⇑F.shift

lim¹ A vanishes if and only if the shift map is surjective.

theorem TauCeti.ModuleTower.mem_range_shift_of_le_map {R : Type u} [Ring R] (F : ModuleTower R) (B : (n : ℕ) → Submodule R ↑(F.obj (Opposite.op n))) (hB : ∀ (n : ℕ), B n ≤ Submodule.map (F.transition n) (B (n + 1))) {c : F.Product} (hc : ∀ (n : ℕ), c n ∈ B n) : c ∈ F.shift.range

If submodules Bₙ ⊆ Aₙ satisfy Bₙ ⊆ φₙ(Bₙ₊₁), then every family (cₙ) with cₙ ∈ Bₙ lies in the image of the shift map.

theorem TauCeti.ModuleTower.shift_surjective {R : Type u} [Ring R] (F : ModuleTower R) (h : ∀ (n : ℕ), Function.Surjective ⇑(F.transition n)) : Function.Surjective ⇑F.shift

If every transition map of a tower is surjective, then so is its shift map.

theorem TauCeti.ModuleTower.subsingleton_limOne_of_surjective {R : Type u} [Ring R] (F : ModuleTower R) (h : ∀ (n : ℕ), Function.Surjective ⇑(F.transition n)) : Subsingleton F.limOne

Towers with surjective transitions have vanishing lim¹ (Stacks, Tag 07KW).

theorem TauCeti.ModuleTower.limπ_surjective {R : Type u} [Ring R] (F : ModuleTower R) (h : ∀ (n : ℕ), Function.Surjective ⇑(F.transition n)) (n : ℕ) : Function.Surjective ⇑(F.limπ n)

If every transition map of a tower is surjective, then so is every projection lim A → Aₙ: an element of Aₙ lifts step by step to a compatible family.

theorem TauCeti.ModuleTower.isSplitEpi_shift {R : Type u} [Ring R] (F : ModuleTower R) (h : ∀ (n : ℕ), CategoryTheory.IsSplitEpi (F.map (CategoryTheory.homOfLE ⋯).op)) : CategoryTheory.IsSplitEpi (ModuleCat.ofHom F.shift)

If every transition map of a tower is a split epimorphism, then so is its shift map.

def TauCeti.ModuleTower.productMap {R : Type u} [Ring R] {F G : ModuleTower R} (f : F ⟶ G) : F.Product →ₗ[R] G.Product

The linear map ∏ₙ Aₙ → ∏ₙ Bₙ induced levelwise by a morphism of towers.

@[simp]

theorem TauCeti.ModuleTower.productMap_apply {R : Type u} [Ring R] {F G : ModuleTower R} (f : F ⟶ G) (x : F.Product) (n : ℕ) : (productMap f) x n = (ModuleCat.Hom.hom (f.app (Opposite.op n))) (x n)

@[simp]

theorem TauCeti.ModuleTower.productMap_id {R : Type u} [Ring R] {F : ModuleTower R} : productMap (CategoryTheory.CategoryStruct.id F) = LinearMap.id

@[simp]

theorem TauCeti.ModuleTower.productMap_comp {R : Type u} [Ring R] {F G H : ModuleTower R} (f : F ⟶ G) (g : G ⟶ H) : productMap (CategoryTheory.CategoryStruct.comp f g) = productMap g ∘ₗ productMap f

theorem TauCeti.ModuleTower.productMap_comp_apply {R : Type u} [Ring R] {F G H : ModuleTower R} (f : F ⟶ G) (g : G ⟶ H) (x : F.Product) : (productMap (CategoryTheory.CategoryStruct.comp f g)) x = (productMap g) ((productMap f) x)

The composition law productMap_comp, applied to a family.

@[simp]

theorem TauCeti.ModuleTower.productMap_zero {R : Type u} [Ring R] {F G : ModuleTower R} : productMap 0 = 0

@[simp]

theorem TauCeti.ModuleTower.productMap_add {R : Type u} [Ring R] {F G : ModuleTower R} (f g : F ⟶ G) : productMap (f + g) = productMap f + productMap g

theorem TauCeti.ModuleTower.coe_productMap {R : Type u} [Ring R] {F G : ModuleTower R} (f : F ⟶ G) : ⇑(productMap f) = Pi.map fun (n : ℕ) => ⇑(ModuleCat.Hom.hom (f.app (Opposite.op n)))

The product map of a morphism of towers is the componentwise map Pi.map.

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

A levelwise injective morphism of towers is injective on products.

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

A levelwise surjective morphism of towers is surjective on products.

theorem TauCeti.ModuleTower.app_comp_transition {R : Type u} [Ring R] {F G : ModuleTower R} (f : F ⟶ G) (n : ℕ) : ModuleCat.Hom.hom (f.app (Opposite.op n)) ∘ₗ F.transition n = G.transition n ∘ₗ ModuleCat.Hom.hom (f.app (Opposite.op (n + 1)))

A morphism of towers commutes with the transition maps.

theorem TauCeti.ModuleTower.app_comp_transitionOfLE {R : Type u} [Ring R] {F G : ModuleTower R} (f : F ⟶ G) {n k : ℕ} (h : n ≤ k) : ModuleCat.Hom.hom (f.app (Opposite.op n)) ∘ₗ F.transitionOfLE h = G.transitionOfLE h ∘ₗ ModuleCat.Hom.hom (f.app (Opposite.op k))

A morphism of towers commutes with the composite transition maps.

theorem TauCeti.ModuleTower.shift_natural {R : Type u} [Ring R] {F G : ModuleTower R} (f : F ⟶ G) : G.shift ∘ₗ productMap f = productMap f ∘ₗ F.shift

The product map of a morphism of towers commutes with the shift maps.

theorem TauCeti.ModuleTower.shift_natural_apply {R : Type u} [Ring R] {F G : ModuleTower R} (f : F ⟶ G) (x : F.Product) : G.shift ((productMap f) x) = (productMap f) (F.shift x)

The naturality square shift_natural, applied to a family.

def TauCeti.ModuleTower.limMap {R : Type u} [Ring R] {F G : ModuleTower R} (f : F ⟶ G) : ↥F.lim →ₗ[R] ↥G.lim

The linear map lim A → lim B induced by a morphism of towers.

@[simp]

theorem TauCeti.ModuleTower.coe_limMap_apply {R : Type u} [Ring R] {F G : ModuleTower R} (f : F ⟶ G) (x : ↥F.lim) : ↑((limMap f) x) = (productMap f) ↑x

@[simp]

theorem TauCeti.ModuleTower.limπ_comp_limMap {R : Type u} [Ring R] {F G : ModuleTower R} (f : F ⟶ G) (n : ℕ) : G.limπ n ∘ₗ limMap f = ModuleCat.Hom.hom (f.app (Opposite.op n)) ∘ₗ F.limπ n

@[simp]

theorem TauCeti.ModuleTower.limMap_id {R : Type u} [Ring R] {F : ModuleTower R} : limMap (CategoryTheory.CategoryStruct.id F) = LinearMap.id

@[simp]

theorem TauCeti.ModuleTower.limMap_comp {R : Type u} [Ring R] {F G H : ModuleTower R} (f : F ⟶ G) (g : G ⟶ H) : limMap (CategoryTheory.CategoryStruct.comp f g) = limMap g ∘ₗ limMap f

@[simp]

theorem TauCeti.ModuleTower.limMap_zero {R : Type u} [Ring R] {F G : ModuleTower R} : limMap 0 = 0

@[simp]

theorem TauCeti.ModuleTower.limMap_add {R : Type u} [Ring R] {F G : ModuleTower R} (f g : F ⟶ G) : limMap (f + g) = limMap f + limMap g

theorem TauCeti.ModuleTower.limMap_inj {R : Type u} [Ring R] {F G : ModuleTower R} (h : ∀ (n : ℕ), Function.Surjective ⇑(F.transition n)) {f g : F ⟶ G} : limMap f = limMap g ↔ f = g

If every transition map of A is surjective, a morphism of towers A ⟶ B is determined by the map it induces on lim: every element of Aₙ lifts to lim A.

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

The first map of the six-term sequence: lim A → lim B is injective when every Aₙ → Bₙ is.

def TauCeti.ModuleTower.limEquivOfIso {R : Type u} [Ring R] {F G : ModuleTower R} (e : F ≅ G) : ↥F.lim ≃ₗ[R] ↥G.lim

The linear equivalence lim A ≃ lim B induced by an isomorphism of towers.

@[simp]

theorem TauCeti.ModuleTower.limEquivOfIso_apply {R : Type u} [Ring R] {F G : ModuleTower R} (e : F ≅ G) (x : ↥F.lim) : (limEquivOfIso e) x = (limMap e.hom) x

@[simp]

theorem TauCeti.ModuleTower.limEquivOfIso_symm_apply {R : Type u} [Ring R] {F G : ModuleTower R} (e : F ≅ G) (x : ↥G.lim) : (limEquivOfIso e).symm x = (limMap e.inv) x

theorem TauCeti.ModuleTower.range_shift_le_comap {R : Type u} [Ring R] {F G : ModuleTower R} (f : F ⟶ G) : F.shift.range ≤ Submodule.comap (productMap f) G.shift.range

A morphism of towers maps the image of the shift map into the image of the shift map.

def TauCeti.ModuleTower.limOneMap {R : Type u} [Ring R] {F G : ModuleTower R} (f : F ⟶ G) : F.limOne →ₗ[R] G.limOne

The linear map lim¹ A → lim¹ B induced by a morphism of towers.

@[simp]

theorem TauCeti.ModuleTower.limOneMap_mk {R : Type u} [Ring R] {F G : ModuleTower R} (f : F ⟶ G) (x : F.Product) : (limOneMap f) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((productMap f) x)

@[simp]

theorem TauCeti.ModuleTower.limOneMap_id {R : Type u} [Ring R] {F : ModuleTower R} : limOneMap (CategoryTheory.CategoryStruct.id F) = LinearMap.id

@[simp]

theorem TauCeti.ModuleTower.limOneMap_comp {R : Type u} [Ring R] {F G H : ModuleTower R} (f : F ⟶ G) (g : G ⟶ H) : limOneMap (CategoryTheory.CategoryStruct.comp f g) = limOneMap g ∘ₗ limOneMap f

@[simp]

theorem TauCeti.ModuleTower.limOneMap_zero {R : Type u} [Ring R] {F G : ModuleTower R} : limOneMap 0 = 0

@[simp]

theorem TauCeti.ModuleTower.limOneMap_add {R : Type u} [Ring R] {F G : ModuleTower R} (f g : F ⟶ G) : limOneMap (f + g) = limOneMap f + limOneMap g

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

The last map of the six-term sequence: lim¹ B → lim¹ C is surjective when every Bₙ → Cₙ is.

def TauCeti.ModuleTower.limOneEquivOfIso {R : Type u} [Ring R] {F G : ModuleTower R} (e : F ≅ G) : F.limOne ≃ₗ[R] G.limOne

The linear equivalence lim¹ A ≃ lim¹ B induced by an isomorphism of towers.

@[simp]

theorem TauCeti.ModuleTower.limOneEquivOfIso_apply {R : Type u} [Ring R] {F G : ModuleTower R} (e : F ≅ G) (x : F.limOne) : (limOneEquivOfIso e) x = (limOneMap e.hom) x

@[simp]

theorem TauCeti.ModuleTower.limOneEquivOfIso_symm_apply {R : Type u} [Ring R] {F G : ModuleTower R} (e : F ≅ G) (x : G.limOne) : (limOneEquivOfIso e).symm x = (limOneMap e.inv) x

def TauCeti.ModuleTower.smulTower {R : Type u} [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] (f : R) : ModuleTower R

The tower M ←f M ←f ⋯ whose transition maps are multiplication by f.

@[simp]

theorem TauCeti.ModuleTower.smulTower_transition {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (f : R) (n : ℕ) : (smulTower M f).transition n = f • LinearMap.id

The transition maps of M ←f M ←f ⋯ are multiplication by f.