Documentation

TauCeti.AlgebraicTopology.ClassifyingSpace.StandardResolution

Milnor's join resolution is homotopy equivalent to the standard resolution #

The ordered chains of Milnor's countable join form a projective resolution TauCeti.universalGSpaceResolution k G of the trivial representation, and Mathlib's standard complex forms another, Rep.standardResolution k G. This file compares them by an explicit map.

Sending an oriented simplex {(i₀, g₀), …, (iₙ, gₙ)} of the countable join, with i₀ < ⋯ < iₙ, to the basis element (g₀, …, gₙ) of the standard complex is a chain map of complexes of representations of G (TauCeti.universalGSpaceChainComplexToStandardComplex). Forgetting the action, it is the module-level comparison TauCeti.universalGSpaceToStandardComplex, degree by degree. It commutes with the two augmentations, which both sum coefficients (TauCeti.universalGSpaceChainComplexToStandardComplex_comp_εToSingle₀), so it lifts the identity of the trivial representation. A lift of the identity between projective resolutions is a homotopy equivalence (TauCeti.universalGSpaceStandardHomotopyEquiv), and it is homotopic to the comparison ProjectiveResolution.homotopyEquiv that Mathlib constructs abstractly from the projectivity of the terms (TauCeti.universalGSpaceChainComplexToStandardComplexHomotopy).

The comparison is a homotopy equivalence and not an isomorphism: for the trivial group and a nonzero coefficient ring, the join has countably many vertices, while the standard complex has a single basis element in degree 0.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.universalGSpaceToStandardHom (k : Type u) [CommRing k] (G : Type u) [Group G] (n : ℕ) :
Rep.ofMulAction k G ((indexedJoin fun (x : ℕ) => G).RealizationCell n) ⟶ Rep.ofMulAction k G (Fin (n + 1) → G)

The explicit comparison in degree n as a morphism of permutation representations: it sends an n-simplex of the countable join to the tuple of its labels, enumerated by increasing index.

Instances For
    source
    @[simp]
    theorem TauCeti.universalGSpaceToStandardHom_hom_single (k : Type u) [CommRing k] (G : Type u) [Group G] {n : ℕ} (c : (indexedJoin fun (x : ℕ) => G).RealizationCell n) (a : k) :
    (Rep.Hom.hom (universalGSpaceToStandardHom k G n)) (MonoidAlgebra.single c a) = MonoidAlgebra.single (universalGSpaceCellLabels c) a

    The comparison sends a simplex to the tuple of its labels.

    source
    noncomputable def TauCeti.universalGSpaceChainComplexToStandardComplex (k : Type u) [CommRing k] (G : Type u) [Group G] :
    universalGSpaceChainComplex k G ⟶ Rep.standardComplex k G

    The join-to-standard chain map of complexes of representations. It sends an oriented simplex {(i₀, g₀), …, (iₙ, gₙ)} of the countable join, with i₀ < ⋯ < iₙ, to the basis element (g₀, …, gₙ) of Mathlib's standard complex.

    Instances For
      source
      theorem TauCeti.universalGSpaceChainComplexToStandardComplex_f (k : Type u) [CommRing k] (G : Type u) [Group G] (n : ℕ) :
      (universalGSpaceChainComplexToStandardComplex k G).f n = CategoryTheory.CategoryStruct.comp (universalGSpaceToStandardHom k G n) (Rep.standardComplex.xIso k G n).inv

      In degree n the chain map is the comparison of permutation representations.

      source
      @[simp]
      theorem TauCeti.universalGSpaceChainComplexToStandardComplex_f_hom_single (k : Type u) [CommRing k] (G : Type u) [Group G] {n : ℕ} (c : (indexedJoin fun (x : ℕ) => G).RealizationCell n) (a : k) :
      (Rep.Hom.hom ((universalGSpaceChainComplexToStandardComplex k G).f n)) (MonoidAlgebra.single c a) = MonoidAlgebra.single (universalGSpaceCellLabels c) a

      In degree n the chain map sends a simplex to the tuple of its labels.

      source
      @[simp]
      theorem TauCeti.universalGSpaceToStandardHom_comp_ε (k : Type u) [CommRing k] (G : Type u) [Group G] :
      CategoryTheory.CategoryStruct.comp (universalGSpaceToStandardHom k G 0) (Rep.standardComplex.ε k G) = permutationAugmentation k G ((indexedJoin fun (x : ℕ) => G).RealizationCell 0)

      In degree 0 the comparison preserves the augmentations: both sum the coefficients.

      source
      @[simp]
      theorem TauCeti.universalGSpaceToStandardHom_comp_ε_assoc (k : Type u) [CommRing k] (G : Type u) [Group G] {Z : Rep.{u, u, u} k G} (h : Rep.trivial k G k ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (universalGSpaceToStandardHom k G 0) (CategoryTheory.CategoryStruct.comp (Rep.standardComplex.ε k G) h) = CategoryTheory.CategoryStruct.comp (permutationAugmentation k G ((indexedJoin fun (x : ℕ) => G).RealizationCell 0)) h

      In degree 0 the comparison preserves the augmentations: both sum the coefficients.

      source
      @[simp]
      theorem TauCeti.universalGSpaceChainComplexToStandardComplex_comp_εToSingle₀ (k : Type u) [CommRing k] (G : Type u) [Group G] :
      CategoryTheory.CategoryStruct.comp (universalGSpaceChainComplexToStandardComplex k G) (Rep.standardComplex.εToSingle₀ k G) = universalGSpaceAugmentation k G

      The join-to-standard chain map preserves the augmentations: both sum the coefficients of a 0-chain.

      source
      @[simp]
      theorem TauCeti.universalGSpaceChainComplexToStandardComplex_comp_εToSingle₀_assoc (k : Type u) [CommRing k] (G : Type u) [Group G] {Z : ChainComplex (Rep.{u, u, u} k G) ℕ} (h : (ChainComplex.single₀ (Rep.{u, u, u} k G)).obj (Rep.trivial k G k) ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (universalGSpaceChainComplexToStandardComplex k G) (CategoryTheory.CategoryStruct.comp (Rep.standardComplex.εToSingle₀ k G) h) = CategoryTheory.CategoryStruct.comp (universalGSpaceAugmentation k G) h

      The join-to-standard chain map preserves the augmentations: both sum the coefficients of a 0-chain.

      source
      theorem TauCeti.universalGSpaceChainComplexToStandardComplex_comp_standardResolution_π (k : Type u) [CommRing k] (G : Type u) [Group G] :
      CategoryTheory.CategoryStruct.comp (universalGSpaceChainComplexToStandardComplex k G) (Rep.standardResolution k G).π = (universalGSpaceResolution k G).π

      The join-to-standard chain map lifts the identity of the trivial representation along the augmentations of the two projective resolutions.

      source
      noncomputable def TauCeti.universalGSpaceStandardHomotopyEquiv (k : Type u) [CommRing k] (G : Type u) [Group G] :
      HomotopyEquiv (universalGSpaceChainComplex k G) (Rep.standardComplex k G)

      Milnor's join resolution is homotopy equivalent to the standard resolution, by a homotopy equivalence whose forward map is the explicit join-to-standard chain map. Its homotopy inverse is the lift of the identity of the trivial representation from the standard resolution to the join resolution.

      Instances For
        source
        @[simp]
        theorem TauCeti.universalGSpaceStandardHomotopyEquiv_hom (k : Type u) [CommRing k] (G : Type u) [Group G] :
        (universalGSpaceStandardHomotopyEquiv k G).hom = universalGSpaceChainComplexToStandardComplex k G

        The forward map of the homotopy equivalence is the join-to-standard chain map.

        source
        @[simp]
        theorem TauCeti.universalGSpaceStandardHomotopyEquiv_inv (k : Type u) [CommRing k] (G : Type u) [Group G] :
        (universalGSpaceStandardHomotopyEquiv k G).inv = CategoryTheory.ProjectiveResolution.lift (CategoryTheory.CategoryStruct.id (Rep.trivial k G k)) (Rep.standardResolution k G) (universalGSpaceResolution k G)

        The homotopy inverse is the lift of the identity of the trivial representation from the standard resolution to the join resolution.

        source
        noncomputable def TauCeti.universalGSpaceChainComplexToStandardComplexHomotopy (k : Type u) [CommRing k] (G : Type u) [Group G] :
        Homotopy (universalGSpaceChainComplexToStandardComplex k G) ((universalGSpaceResolution k G).homotopyEquiv (Rep.standardResolution k G)).hom

        The join-to-standard chain map is homotopic to Mathlib's comparison of the two projective resolutions, the lift of the identity of the trivial representation constructed by ProjectiveResolution.homotopyEquiv.

        Instances For