Theorems · Definition · commutative algebra

Module.DirectLimit.congr

{R : Type u_1} →
  [inst : Semiring R] →
    {ι : Type u_2} →
      [inst_1 : Preorder ι] →
        {G : ι → Type u_3} →
          [inst_2 : (i : ι) → AddCommMonoid (G i)] →
            [inst_3 : (i : ι) → Module R (G i)] →
              {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j} →
                [inst_4 : DecidableEq ι] →
                  {G' : ι → Type u_5} →
                    [inst_5 : (i : ι) → AddCommMonoid (G' i)] →
                      [inst_6 : (i : ι) → Module R (G' i)] →
                        {f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j} →
                          (e : (i : ι) → G i ≃ₗ[R] G' i) →
                            (∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)) →
                              Module.DirectLimit G f ≃ₗ[R] Module.DirectLimit G' f'

Consider direct limits lim G and lim G' with direct system f and f' respectively, any family of equivalences eᵢ : Gᵢ ≅ G'ᵢ such that e ∘ f = f' ∘ e induces an equivalence lim G ≅ lim G'.

Defined in

Mathlib.Algebra.Colimit.Module

Cited by

4 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringPreorderAddCommMonoidModuleDecidableEqAddCommMonoidModule