Documentation

TauCeti.Algebra.Module.Torsion.Snake

The kernel–cokernel exact sequence of multiplication by a scalar #

Let r be an element of a commutative ring R. Multiplication by r is an endomorphism of every R-module M; its kernel is the r-torsion M[r] = Submodule.torsionBy R M r and its cokernel is M ⧸ rM = QuotSMulTop r M. For a short exact sequence 0 → M₁ → M₂ → M₃ → 0 of R-modules the snake lemma, applied to multiplication by r on the three terms, gives the six-term exact sequence

0 → M₁[r] → M₂[r] → M₃[r] → M₁ ⧸ rM₁ → M₂ ⧸ rM₂ → M₃ ⧸ rM₃ → 0.

The functor QuotSMulTop r and the right-exact half of this sequence are Mathlib's (QuotSMulTop.map, QuotSMulTop.map_exact, QuotSMulTop.map_surjective). This file supplies the torsion functor TauCeti.torsionByMap, the left-exact half, the connecting map TauCeti.torsionByδ (Mathlib's SnakeLemma.δ' for this diagram), exactness at its two ends, and its naturality in morphisms of short exact sequences.

Naturality is what makes the connecting map compatible with extra structure. For R = ℤ, r = ℓ and a group G acting on the sequence by additive automorphisms, each g : G gives a morphism of the sequence to itself, and TauCeti.torsionByδ_comp_torsionByMap says that the connecting map commutes with the actions of g on M₃[ℓ] and on M₁ ⧸ ℓM₁. This is the form in which the sequence enters the comparison of M ⧸ ℓM with M[ℓ] for G-modules in Neukirch–Schmidt–Wingberg, Cohomology of Number Fields, (7.3.3).

Main definitions #

Main results #

source
def TauCeti.torsionByMap {R : Type u_1} [CommSemiring R] (r : R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) :
↥(Submodule.torsionBy R M r) →ₗ[R] ↥(Submodule.torsionBy R N r)

A linear map carries r-torsion to r-torsion; this is its restriction M[r] →ₗ[R] N[r], the action on morphisms of the functor M ↦ M[r] dual to QuotSMulTop.map.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.coe_torsionByMap_apply {R : Type u_1} [CommSemiring R] (r : R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (x : ↥(Submodule.torsionBy R M r)) :
    ↑((torsionByMap r f) x) = f ↑x
    source
    @[simp]
    theorem TauCeti.torsionByMap_id {R : Type u_1} [CommSemiring R] (r : R) {M : Type u_2} [AddCommMonoid M] [Module R M] :
    torsionByMap r LinearMap.id = LinearMap.id
    source
    theorem TauCeti.torsionByMap_comp {R : Type u_1} [CommSemiring R] (r : R) {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (g : N →ₗ[R] P) (f : M →ₗ[R] N) :
    torsionByMap r (g ∘ₗ f) = torsionByMap r g ∘ₗ torsionByMap r f
    source
    theorem TauCeti.subtype_comp_torsionByMap {R : Type u_1} [CommSemiring R] (r : R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) :
    (Submodule.torsionBy R N r).subtype ∘ₗ torsionByMap r f = f ∘ₗ (Submodule.torsionBy R M r).subtype

    The inclusion of the r-torsion intertwines torsionByMap with the map itself.

    source
    theorem TauCeti.exact_subtype_torsionBy {R : Type u_1} [CommSemiring R] (r : R) (M : Type u_2) [AddCommMonoid M] [Module R M] :
    Function.Exact ⇑(Submodule.torsionBy R M r).subtype ⇑(DistribSMul.toLinearMap R M r)

    The r-torsion is the kernel of multiplication by r.

    source
    theorem TauCeti.injective_torsionByMap {R : Type u_1} [CommSemiring R] {r : R} {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M →ₗ[R] N} (hf : Function.Injective ⇑f) :
    Function.Injective ⇑(torsionByMap r f)

    The restriction of an injective linear map to the r-torsion is injective.

    source
    theorem TauCeti.exact_torsionByMap {R : Type u_1} [CommSemiring R] {r : R} {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) :
    Function.Exact ⇑(torsionByMap r f) ⇑(torsionByMap r g)

    Left exactness of r-torsion: if f is injective and f, g are exact, then so are M[r] → N[r] → P[r]. Only the injectivity of f is used, not the surjectivity of g.

    source
    theorem TauCeti.exact_toLinearMap_mkQ {R : Type u_1} [CommRing R] (r : R) (M : Type u_5) [AddCommGroup M] [Module R M] :
    Function.Exact ⇑(DistribSMul.toLinearMap R M r) ⇑(r • ⊤).mkQ

    M ⧸ rM is the cokernel of multiplication by r.

    source
    noncomputable def TauCeti.torsionByδ {R : Type u_1} [CommRing R] (r : R) {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃] {f : M₁ →ₗ[R] M₂} {g : M₂ →ₗ[R] M₃} (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) :
    ↥(Submodule.torsionBy R M₃ r) →ₗ[R] QuotSMulTop r M₁

    The connecting map M₃[r] → M₁ ⧸ rM₁ of a short exact sequence 0 → M₁ → M₂ → M₃ → 0: Mathlib's snake-lemma map SnakeLemma.δ' for multiplication by r on the three terms. It is characterized by TauCeti.torsionByδ_eq: lift x to y ∈ M₂, write r • y = f z, and take the class of z.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem TauCeti.torsionByδ_eq {R : Type u_1} [CommRing R] {r : R} {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃] {f : M₁ →ₗ[R] M₂} {g : M₂ →ₗ[R] M₃} (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) (x : ↥(Submodule.torsionBy R M₃ r)) {y : M₂} (hy : g y = ↑x) {z : M₁} (hz : f z = r • y) :
      (torsionByδ r hfg hf hg) x = Submodule.Quotient.mk z

      The characterization of the connecting map: if g y = x and f z = r • y, then the connecting map sends x to the class of z.

      source
      theorem TauCeti.exact_torsionByMap_torsionByδ {R : Type u_1} [CommRing R] {r : R} {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃] {f : M₁ →ₗ[R] M₂} {g : M₂ →ₗ[R] M₃} (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) :
      Function.Exact ⇑(torsionByMap r g) ⇑(torsionByδ r hfg hf hg)

      Exactness at M₃[r]: the kernel of the connecting map is the image of M₂[r].

      source
      theorem TauCeti.exact_torsionByδ_quotSMulTop_map {R : Type u_1} [CommRing R] {r : R} {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃] {f : M₁ →ₗ[R] M₂} {g : M₂ →ₗ[R] M₃} (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) :
      Function.Exact ⇑(torsionByδ r hfg hf hg) ⇑((QuotSMulTop.map r) f)

      Exactness at M₁ ⧸ rM₁: the kernel of M₁ ⧸ rM₁ → M₂ ⧸ rM₂ is the image of the connecting map.

      source
      theorem TauCeti.finite_quotSMulTop_of_exact {R : Type u_1} [CommRing R] {r : R} {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃] {f : M₁ →ₗ[R] M₂} {g : M₂ →ₗ[R] M₃} (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) [Finite ↥(Submodule.torsionBy R M₃ r)] [Finite (QuotSMulTop r M₂)] :
      Finite (QuotSMulTop r M₁)

      Finiteness of M₁ ⧸ rM₁ along a short exact sequence: if M₃[r] and M₂ ⧸ rM₂ are finite, so is M₁ ⧸ rM₁, which sits between them in the six-term sequence.

      source
      theorem TauCeti.torsionByδ_comp_torsionByMap {R : Type u_1} [CommRing R] {r : R} {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃] {f : M₁ →ₗ[R] M₂} {g : M₂ →ₗ[R] M₃} {N₁ : Type u_5} {N₂ : Type u_6} {N₃ : Type u_7} [AddCommGroup N₁] [Module R N₁] [AddCommGroup N₂] [Module R N₂] [AddCommGroup N₃] [Module R N₃] {f' : N₁ →ₗ[R] N₂} {g' : N₂ →ₗ[R] N₃} (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) (hfg' : Function.Exact ⇑f' ⇑g') (hf' : Function.Injective ⇑f') (hg' : Function.Surjective ⇑g') {α : M₁ →ₗ[R] N₁} {β : M₂ →ₗ[R] N₂} {γ : M₃ →ₗ[R] N₃} (hαβ : β ∘ₗ f = f' ∘ₗ α) (hβγ : γ ∘ₗ g = g' ∘ₗ β) :
      torsionByδ r hfg' hf' hg' ∘ₗ torsionByMap r γ = (QuotSMulTop.map r) α ∘ₗ torsionByδ r hfg hf hg

      Naturality of the connecting map: a morphism (α, β, γ) of short exact sequences intertwines the two connecting maps, δ' ∘ γ[r] = (α mod r) ∘ δ.