Theorems · Definition · category theory

Profinite.NobelingProof.GoodProducts.SumEval

{I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] →
      [inst_1 : WellFoundedLT I] →
        {o : Ordinal.{u}} →
          (ho : o < Ordinal.type fun x1 x2 => x1 < x2) →
            ↑(Profinite.NobelingProof.GoodProducts
                    (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)) ⊕
                ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho) →
              LocallyConstant ↑C ℤ

Let N := LocallyConstant (π C (ord I · < o)) ℤ M := LocallyConstant C ℤ P := LocallyConstant (C' C ho) ℤ ι := GoodProducts (π C (ord I · < o)) ι' := GoodProducts (C' C ho') v : ι → N := GoodProducts.eval (π C (ord I · < o)) Then SumEval C ho is the map u in the diagram below. It is linearly independent if and only if GoodProducts.eval C is, see linearIndependent_iff_sum. The top row is the exact sequence given by succ_exact and succ_mono. The left square commutes by GoodProducts.square_commutes. `` 0 --→ N --→ M --→ P ↑ ↑ ↑ v| u| | ι → ι ⊕ ι' ← ι' ``

Defined in

Mathlib.Topology.Category.Profinite.Nobeling.Successor

Cited by

3 results in Mathlib

Foundations

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

Assumes

LinearOrderWellFoundedLT