Cellular chains with a monoid action #
A family of cellular self-maps satisfying the action laws induces representations on cellular
chains. Naturality of the cellular differential assembles these into a complex in Rep.
The forgetful isomorphism identifies it with the original cellular chain complex.
The maps act on the CW subset itself; no extension to its ambient space or compatibility with chosen characteristic maps is required.
noncomputable def
TauCeti.cellularActionRepresentation
{X : Type u}
[TopologicalSpace X]
[T2Space X]
(C : Set X)
[Topology.CWComplex C]
{G : Type u}
[Monoid G]
(ρ : G → (↧↑C ⟶ ↧↑C))
(hcell : ∀ (g : G), IsCellular C C (ρ g))
(hone : ρ 1 = CategoryTheory.CategoryStruct.id ↧↑C)
(hmul : ∀ (g h : G), ρ (g * h) = CategoryTheory.CategoryStruct.comp (ρ h) (ρ g))
(R : Type u)
[Ring R]
(n : ℕ)
:
Representation R G ↑(cellularChainGroup C (↧R) n)
The representation induced on cellular chains by a cellular action.
Instances For
@[simp]
theorem
TauCeti.cellularActionRepresentation_apply
{X : Type u}
[TopologicalSpace X]
[T2Space X]
(C : Set X)
[Topology.CWComplex C]
{G : Type u}
[Monoid G]
(ρ : G → (↧↑C ⟶ ↧↑C))
(hcell : ∀ (g : G), IsCellular C C (ρ g))
(hone : ρ 1 = CategoryTheory.CategoryStruct.id ↧↑C)
(hmul : ∀ (g h : G), ρ (g * h) = CategoryTheory.CategoryStruct.comp (ρ h) (ρ g))
(R : Type u)
[Ring R]
(n : ℕ)
(g : G)
:
(cellularActionRepresentation C ρ hcell hone hmul R n) g = ModuleCat.Hom.hom (cellularChainGroupMap C C ⋯ (↧R) n)
The action is induced by the given cellular self-map.
noncomputable def
TauCeti.cellularActionDifferential
{X : Type u}
[TopologicalSpace X]
[T2Space X]
(C : Set X)
[Topology.CWComplex C]
{G : Type u}
[Monoid G]
(ρ : G → (↧↑C ⟶ ↧↑C))
(hcell : ∀ (g : G), IsCellular C C (ρ g))
(hone : ρ 1 = CategoryTheory.CategoryStruct.id ↧↑C)
(hmul : ∀ (g h : G), ρ (g * h) = CategoryTheory.CategoryStruct.comp (ρ h) (ρ g))
(R : Type u)
[Ring R]
(n : ℕ)
:
Rep.of (cellularActionRepresentation C ρ hcell hone hmul R (n + 1)) ⟶ Rep.of (cellularActionRepresentation C ρ hcell hone hmul R n)
The cellular differential as a morphism of representations.
Instances For
@[simp]
theorem
TauCeti.cellularActionDifferential_hom_toLinearMap
{X : Type u}
[TopologicalSpace X]
[T2Space X]
(C : Set X)
[Topology.CWComplex C]
{G : Type u}
[Monoid G]
(ρ : G → (↧↑C ⟶ ↧↑C))
(hcell : ∀ (g : G), IsCellular C C (ρ g))
(hone : ρ 1 = CategoryTheory.CategoryStruct.id ↧↑C)
(hmul : ∀ (g h : G), ρ (g * h) = CategoryTheory.CategoryStruct.comp (ρ h) (ρ g))
(R : Type u)
[Ring R]
(n : ℕ)
:
(Rep.Hom.hom (cellularActionDifferential C ρ hcell hone hmul R n)).toLinearMap = ModuleCat.Hom.hom (cellularDifferential C (↧R) n)
The underlying linear map is the cellular differential.
noncomputable def
TauCeti.cellularActionComplex
{X : Type u}
[TopologicalSpace X]
[T2Space X]
(C : Set X)
[Topology.CWComplex C]
{G : Type u}
[Monoid G]
(ρ : G → (↧↑C ⟶ ↧↑C))
(hcell : ∀ (g : G), IsCellular C C (ρ g))
(hone : ρ 1 = CategoryTheory.CategoryStruct.id ↧↑C)
(hmul : ∀ (g h : G), ρ (g * h) = CategoryTheory.CategoryStruct.comp (ρ h) (ρ g))
(R : Type u)
[Ring R]
:
ChainComplex (Rep R G) ℕ
Cellular chains retaining a cellular monoid action.
Instances For
@[simp]
theorem
TauCeti.cellularActionComplex_X
{X : Type u}
[TopologicalSpace X]
[T2Space X]
(C : Set X)
[Topology.CWComplex C]
{G : Type u}
[Monoid G]
(ρ : G → (↧↑C ⟶ ↧↑C))
(hcell : ∀ (g : G), IsCellular C C (ρ g))
(hone : ρ 1 = CategoryTheory.CategoryStruct.id ↧↑C)
(hmul : ∀ (g h : G), ρ (g * h) = CategoryTheory.CategoryStruct.comp (ρ h) (ρ g))
(R : Type u)
[Ring R]
(n : ℕ)
:
(cellularActionComplex C ρ hcell hone hmul R).X n = Rep.of (cellularActionRepresentation C ρ hcell hone hmul R n)
The terms of the equivariant cellular complex.
@[simp]
theorem
TauCeti.cellularActionComplex_d
{X : Type u}
[TopologicalSpace X]
[T2Space X]
(C : Set X)
[Topology.CWComplex C]
{G : Type u}
[Monoid G]
(ρ : G → (↧↑C ⟶ ↧↑C))
(hcell : ∀ (g : G), IsCellular C C (ρ g))
(hone : ρ 1 = CategoryTheory.CategoryStruct.id ↧↑C)
(hmul : ∀ (g h : G), ρ (g * h) = CategoryTheory.CategoryStruct.comp (ρ h) (ρ g))
(R : Type u)
[Ring R]
(n : ℕ)
:
(cellularActionComplex C ρ hcell hone hmul R).d (n + 1) n = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(CategoryTheory.CategoryStruct.comp (cellularActionDifferential C ρ hcell hone hmul R n) (CategoryTheory.eqToHom ⋯))
Its differential is the equivariant cellular differential.
noncomputable def
TauCeti.cellularActionComplexForget₂Iso
{X : Type u}
[TopologicalSpace X]
[T2Space X]
(C : Set X)
[Topology.CWComplex C]
{G : Type u}
[Monoid G]
(ρ : G → (↧↑C ⟶ ↧↑C))
(hcell : ∀ (g : G), IsCellular C C (ρ g))
(hone : ρ 1 = CategoryTheory.CategoryStruct.id ↧↑C)
(hmul : ∀ (g h : G), ρ (g * h) = CategoryTheory.CategoryStruct.comp (ρ h) (ρ g))
(R : Type u)
[Ring R]
:
cellularChainComplex C ↧R ≅ ((CategoryTheory.forget₂ (Rep R G) (ModuleCat R)).mapHomologicalComplex (ComplexShape.down ℕ)).obj
(cellularActionComplex C ρ hcell hone hmul R)
Forgetting the action recovers the geometric cellular chain complex.
Instances For
@[simp]
theorem
TauCeti.cellularActionComplexForget₂Iso_hom_f
{X : Type u}
[TopologicalSpace X]
[T2Space X]
(C : Set X)
[Topology.CWComplex C]
{G : Type u}
[Monoid G]
(ρ : G → (↧↑C ⟶ ↧↑C))
(hcell : ∀ (g : G), IsCellular C C (ρ g))
(hone : ρ 1 = CategoryTheory.CategoryStruct.id ↧↑C)
(hmul : ∀ (g h : G), ρ (g * h) = CategoryTheory.CategoryStruct.comp (ρ h) (ρ g))
(R : Type u)
[Ring R]
(n : ℕ)
:
Components of the forgetful identification are the canonical cellular-term transports.
@[simp]
theorem
TauCeti.cellularActionComplexForget₂Iso_inv_f
{X : Type u}
[TopologicalSpace X]
[T2Space X]
(C : Set X)
[Topology.CWComplex C]
{G : Type u}
[Monoid G]
(ρ : G → (↧↑C ⟶ ↧↑C))
(hcell : ∀ (g : G), IsCellular C C (ρ g))
(hone : ρ 1 = CategoryTheory.CategoryStruct.id ↧↑C)
(hmul : ∀ (g h : G), ρ (g * h) = CategoryTheory.CategoryStruct.comp (ρ h) (ρ g))
(R : Type u)
[Ring R]
(n : ℕ)
:
Inverse components of the forgetful identification are the reverse term transports.