Module

SequentialLimit.lean

Nyll.EtaleCohomology.Classical.SequentialLimit

2 declarations indexed from sourceView source ↗

Module documentation

Compatible families in a sequence of abelian groups

The inverse limit is a subgroup of the product. Keeping its group operations independent of the concrete Ext groups avoids unfolding cohomology constructions when checking the elementary compatibility equations.

Imports2

Mathlib.Algebra.Group.Subgroup.Defs
Mathlib.Algebra.Group.Pi.Basic

Imported by2

def

sequentialLimit

L23 ↗

EtaleCohomology.Classical.sequentialLimit

Documentation

The inverse limit subgroup for a sequence of additive transition maps.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace EtaleCohomology.Classical
universe u

Lean source · full declaration

def sequentialLimit (M : ℕ → Type u) [∀ n, AddCommGroup (M n)]
    (r : ∀ n, M (n + 1) →+ M n) : AddSubgroup (∀ n, M n) where
  carrier := {a | ∀ n, r n (a (n + 1)) = a n}
  zero_mem' := fun n => map_zero (r n)
  add_mem' ha hb n := (map_add (r n) _ _).trans (congrArg₂ (· + ·) (ha n) (hb n))
  neg_mem' ha n := (map_neg (r n) _).trans (congrArg Neg.neg (ha n))

def

sequentialLimitProjection

L31 ↗

EtaleCohomology.Classical.sequentialLimitProjection