The graded module of the coinduced resolution

The shifted canonical resolution has degree-n term C(G, …, C(G, X)), with n + 1 function-space layers. Its external direct sum carries the canonical square-zero differential of degree one and the componentwise G-action. The augmentation includes X as constant functions in degree zero. A compatible pair, a continuous homomorphism φ : H →ₜ* G with a morphism f : res φ X ⟶ Y, acts degreewise through Mathlib's resolution maps F ↦ f ∘ F ∘ φ; coefficient morphisms are the case φ = id. This change of group is how restriction and inflation reach cocycles written on the total module.

For a compact group, a discrete scalar ring R, and smooth discrete coefficients, the total module with its discrete topology is again smooth. This provides a graded coefficient module for finite tensor induction of resolutions; tensor products can apply the differential on one carrier while tracking its degree.

Evaluation at 1 contracts the total module onto the coefficients. The projection π evaluates the degree-zero component at 1, and the homotopy h, of degree minus one, is the total map of the contraction TopRep.resolutionModuleHomotopy of the underlying complex. Together with the augmentation ι they satisfy π ∘ ι = 1 and d ∘ h + h ∘ d = 1 - ι ∘ π. Neither π nor h is equivariant. Being linear data on one carrier, this contraction can be tensored factor by factor to contract a tensor power of total resolutions onto the tensor power of the coefficients.

Main results

• gradedResolutionTopRepDifferential bundles the square-zero differential as a morphism of discrete topological representations.
• gradedResolutionTopRepAugmentation includes discrete coefficients into the degree-zero term as a morphism of topological representations, naturally in the coefficients.
• gradedResolutionMap is the map of a compatible pair; it commutes with the differentials, the augmentations, the projections and the contracting homotopies, preserves degrees, and composes along composite pairs.
• gradedResolutionTopRepMap bundles coefficient maps, preserving identities, composition, and the differential.
• gradedResolutionTopRepResMap bundles the map of a compatible pair as a morphism from the restricted total resolution, of degree zero and commuting with the differentials and the augmentations.
• TauCeti.smoothGradedResolutionFunctor packages the smooth total resolution functorially.
• TauCeti.smoothGradedResolutionAugmentation is its natural coefficient augmentation, and TauCeti.smoothGradedResolutionDifferential its differential.
• TauCeti.smoothGradedResolutionResMap compares the restriction of the smooth total resolution along a continuous homomorphism with the smooth total resolution of the restriction.
• gradedResolutionProjection and gradedResolutionHomotopy contract the total resolution: gradedResolutionProjection_augmentation and gradedResolutionDifferential_gradedResolutionHomotopy_add are the contraction identities, and both maps are natural in the coefficients; gradedResolutionProjection_eq_zero_of_mem and gradedResolutionHomotopy_eq_zero_of_mem_zero say that they vanish in nonzero and in zero degree.
• gradedResolutionModule_add_self_eq_zero: the total resolution of coefficients that are their own additive inverses has the same property.

References

• L. Evens, A generalization of the transfer map in the cohomology of groups, Transactions of the American Mathematical Society 108 (1963), §§2–5.
• Mathlib's TopRep.resolution', ContinuousCohomology.resolutionMap, and Representation.directSum supply the resolution, coefficient maps, and total action.

@[reducible, inline]

abbrev TopRep.gradedResolutionModule {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : Type (max v w)

The direct sum of the shifted coinduced resolution. Degree zero is C(G, X).

@[instance_reducible]

noncomputable def TopRep.GradedResolution.instModule {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : Module R X.gradedResolutionModule

The componentwise scalar action on the total resolution. Open this scope when tensoring resolutions: for integer scalars, the fallback action on the underlying additive group need not be definitionally equal to this direct-sum action.

noncomputable def TopRep.gradedResolutionDifferential {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : X.gradedResolutionModule →ₗ[R] X.gradedResolutionModule

The canonical differential on the total shifted resolution.

theorem TopRep.gradedResolutionDifferential_lof {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DecidableEq ℕ] (n : ℕ) (x : ↑(X.resolutionX (n + 1))) : X.gradedResolutionDifferential ((DirectSum.lof R ℕ (fun (n : ℕ) => ↑(X.resolutionX (n + 1))) n) x) = (DirectSum.lof R ℕ (fun (n : ℕ) => ↑(X.resolutionX (n + 1))) (n + 1)) ((Hom.hom (X.d (n + 1))) x)

On degree n, the total differential is the original resolution differential d (n + 1).

@[simp]

theorem TopRep.gradedResolutionDifferential_sq {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) (x : X.gradedResolutionModule) : X.gradedResolutionDifferential (X.gradedResolutionDifferential x) = 0

The differential of the total shifted resolution squares to zero.

theorem TopRep.gradedResolutionModule_add_self_eq_zero {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) (hX : ∀ (x : ↑X), x + x = 0) (z : X.gradedResolutionModule) : z + z = 0

If every coefficient is its own additive inverse, then so is every element of the total resolution.

noncomputable def TopRep.gradedResolutionPiece {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : ℤ → Submodule R X.gradedResolutionModule

The integer homogeneous-piece family of the total resolution, zero in negative degrees.

theorem TopRep.isInternal_gradedResolutionPiece {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : DirectSum.IsInternal X.gradedResolutionPiece

The homogeneous resolution terms decompose the total resolution as an internal direct sum.

@[simp]

theorem TopRep.gradedResolutionPiece_natCast {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DecidableEq ℕ] (n : ℕ) : X.gradedResolutionPiece ↑n = (DirectSum.lof R ℕ (fun (n : ℕ) => ↑(X.resolutionX (n + 1))) n).range

In a nonnegative degree, the homogeneous piece is the corresponding resolution term's copy.

theorem TopRep.gradedResolutionPiece_of_neg {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) {p : ℤ} (hp : p < 0) : X.gradedResolutionPiece p = ⊥

The total resolution has no negative homogeneous pieces.

theorem TopRep.lof_mem_gradedResolutionPiece {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DecidableEq ℕ] (n : ℕ) (x : ↑(X.resolutionX (n + 1))) : (DirectSum.lof R ℕ (fun (n : ℕ) => ↑(X.resolutionX (n + 1))) n) x ∈ X.gradedResolutionPiece ↑n

Inclusion of a resolution term gives an element in its homogeneous degree.

theorem TopRep.isHomogeneous_gradedResolutionDifferential {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : TauCeti.LinearMap.IsHomogeneous X.gradedResolutionDifferential X.gradedResolutionPiece X.gradedResolutionPiece 1

The total resolution differential has degree one.

noncomputable def TopRep.gradedResolutionRepresentation {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : Representation R G X.gradedResolutionModule

The componentwise group representation on the total shifted coinduced resolution.

theorem TopRep.gradedResolutionRepresentation_lof {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DecidableEq ℕ] (n : ℕ) (g : G) (x : ↑(X.resolutionX (n + 1))) : (X.gradedResolutionRepresentation g) ((DirectSum.lof R ℕ (fun (n : ℕ) => ↑(X.resolutionX (n + 1))) n) x) = (DirectSum.lof R ℕ (fun (n : ℕ) => ↑(X.resolutionX (n + 1))) n) (((X.resolutionX (n + 1)).ρ g) x)

The group action on an included term is its original resolution action.

@[simp]

theorem TopRep.component_gradedResolutionRepresentation {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) (n : ℕ) (g : G) (v : X.gradedResolutionModule) : (DirectSum.component R ℕ (fun (n : ℕ) => ↑(X.resolutionX (n + 1))) n) ((X.gradedResolutionRepresentation g) v) = ((X.resolutionX (n + 1)).ρ g) ((DirectSum.component R ℕ (fun (n : ℕ) => ↑(X.resolutionX (n + 1))) n) v)

The degree-n component of g • v is g applied to the degree-n component of v.

theorem TopRep.gradedResolutionDifferential_equivariant {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) (g : G) (x : X.gradedResolutionModule) : X.gradedResolutionDifferential ((X.gradedResolutionRepresentation g) x) = (X.gradedResolutionRepresentation g) (X.gradedResolutionDifferential x)

The total resolution differential is equivariant.

theorem TopRep.isHomogeneous_gradedResolutionRepresentation {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) (g : G) : TauCeti.LinearMap.IsHomogeneous (X.gradedResolutionRepresentation g) X.gradedResolutionPiece X.gradedResolutionPiece 0

The componentwise action preserves the homogeneous pieces.

def TopRep.gradedResolutionAugmentation {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : ↑X →ₗ[R] X.gradedResolutionModule

The augmentation of X into the degree-zero term of the total shifted resolution.

@[simp]

theorem TopRep.gradedResolutionAugmentation_apply {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [h : DecidableEq ℕ] (x : ↑X) : X.gradedResolutionAugmentation x = (DirectSum.lof R ℕ (fun (n : ℕ) => ↑(X.resolutionX (n + 1))) 0) ((Hom.hom (X.d 0)) x)

The augmentation includes the constant resolution element in degree zero.

theorem TopRep.gradedResolutionAugmentation_mem {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) (x : ↑X) : X.gradedResolutionAugmentation x ∈ X.gradedResolutionPiece 0

The augmentation takes values in degree zero.

@[simp]

theorem TopRep.gradedResolutionDifferential_augmentation {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) (x : ↑X) : X.gradedResolutionDifferential (X.gradedResolutionAugmentation x) = 0

The augmentation takes values in the kernel of the differential.

theorem TopRep.gradedResolutionAugmentation_equivariant {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) (g : G) (x : ↑X) : X.gradedResolutionAugmentation ((X.ρ g) x) = (X.gradedResolutionRepresentation g) (X.gradedResolutionAugmentation x)

The augmentation is equivariant for the original action on X.

theorem TopRep.gradedResolutionAugmentation_injective {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : Function.Injective ⇑X.gradedResolutionAugmentation

The augmentation embeds the coefficient module.

noncomputable def TopRep.gradedResolutionMap {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) {Y : TopRep R H} (f : res (↑φ) X ⟶ Y) : X.gradedResolutionModule →ₗ[R] Y.gradedResolutionModule

The map of the total shifted resolutions induced by a compatible pair: a continuous homomorphism φ : H →ₜ* G and a morphism f : res φ X ⟶ Y. It is Mathlib's ContinuousCohomology.resolutionMap φ f, F ↦ f ∘ F ∘ φ, in every degree. At φ = id it is the map induced by a coefficient morphism.

theorem TopRep.gradedResolutionMap_lof {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) {Y : TopRep R H} [DecidableEq ℕ] (f : res (↑φ) X ⟶ Y) (n : ℕ) (x : ↑(X.resolutionX (n + 1))) : (gradedResolutionMap φ f) ((DirectSum.lof R ℕ (fun (n : ℕ) => ↑(X.resolutionX (n + 1))) n) x) = (DirectSum.lof R ℕ (fun (n : ℕ) => ↑(Y.resolutionX (n + 1))) n) ((Hom.hom (ContinuousCohomology.resolutionMap φ f (n + 1))) x)

The map of a compatible pair acts on an included term by Mathlib's resolution map.

theorem TopRep.gradedResolutionMap_differential {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) {Y : TopRep R H} (f : res (↑φ) X ⟶ Y) (x : X.gradedResolutionModule) : (gradedResolutionMap φ f) (X.gradedResolutionDifferential x) = Y.gradedResolutionDifferential ((gradedResolutionMap φ f) x)

The map of a compatible pair commutes with the total differentials.

theorem TopRep.gradedResolutionMap_differential_eq_zero {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) {Y : TopRep R H} (f : res (↑φ) X ⟶ Y) {x : X.gradedResolutionModule} (hx : X.gradedResolutionDifferential x = 0) : Y.gradedResolutionDifferential ((gradedResolutionMap φ f) x) = 0

The map of a compatible pair carries cocycles to cocycles.

@[simp]

theorem TopRep.gradedResolutionMap_augmentation {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) {Y : TopRep R H} (f : res (↑φ) X ⟶ Y) (x : ↑X) : (gradedResolutionMap φ f) (X.gradedResolutionAugmentation x) = Y.gradedResolutionAugmentation ((Hom.hom f) x)

The map of a compatible pair carries the augmentation of x to the augmentation of f x.

theorem TopRep.isHomogeneous_gradedResolutionMap {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) {Y : TopRep R H} (f : res (↑φ) X ⟶ Y) : TauCeti.LinearMap.IsHomogeneous (gradedResolutionMap φ f) X.gradedResolutionPiece Y.gradedResolutionPiece 0

The map of a compatible pair preserves the homogeneous degrees of the total resolutions.

theorem TopRep.gradedResolutionMap_mem_piece {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) {Y : TopRep R H} (f : res (↑φ) X ⟶ Y) {n : ℕ} {x : X.gradedResolutionModule} (hx : x ∈ X.gradedResolutionPiece ↑n) : (gradedResolutionMap φ f) x ∈ Y.gradedResolutionPiece ↑n

The map of a compatible pair preserves each homogeneous piece of the total resolution.

theorem TopRep.gradedResolutionMap_equivariant {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) {Y : TopRep R H} (f : res (↑φ) X ⟶ Y) (h : H) (x : X.gradedResolutionModule) : (gradedResolutionMap φ f) ((X.gradedResolutionRepresentation (φ h)) x) = (Y.gradedResolutionRepresentation h) ((gradedResolutionMap φ f) x)

The map of a compatible pair intertwines the action of φ h on the total resolution of X with the action of h on that of Y.

theorem TopRep.gradedResolutionMap_invariant {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) {Y : TopRep R H} (f : res (↑φ) X ⟶ Y) {x : X.gradedResolutionModule} (hx : ∀ (g : G), (X.gradedResolutionRepresentation g) x = x) (h : H) : (Y.gradedResolutionRepresentation h) ((gradedResolutionMap φ f) x) = (gradedResolutionMap φ f) x

The map of a compatible pair carries invariant elements to invariant elements.

@[simp]

theorem TopRep.gradedResolutionMap_id {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} : gradedResolutionMap (ContinuousMonoidHom.id G) (CategoryTheory.CategoryStruct.id X) = LinearMap.id

Identity coefficients induce the identity on the total resolution.

theorem TopRep.gradedResolutionMap_comp {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {H K : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [Group K] [TopologicalSpace K] [IsTopologicalGroup K] (φ : H →ₜ* G) {Y : TopRep R H} (ψ : K →ₜ* H) {Z : TopRep R K} (f : res (↑φ) X ⟶ Y) (g : res (↑ψ) Y ⟶ Z) : gradedResolutionMap (φ.comp ψ) (CategoryTheory.CategoryStruct.comp ((resFunctor ↑ψ).map f) g) = gradedResolutionMap ψ g ∘ₗ gradedResolutionMap φ f

The maps of compatible pairs compose on the total resolutions.

noncomputable def TopRep.gradedResolutionProjection {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : X.gradedResolutionModule →ₗ[R] ↑X

The projection of the total shifted resolution onto its coefficients: evaluation at 1 of the degree-zero component. It retracts the augmentation, but it is not equivariant.

@[simp]

theorem TopRep.gradedResolutionProjection_lof_zero {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [h : DecidableEq ℕ] (F : ↑(X.resolutionX 1)) : X.gradedResolutionProjection ((DirectSum.lof R ℕ (fun (n : ℕ) => ↑(X.resolutionX (n + 1))) 0) F) = F 1

The projection evaluates a degree-zero term at 1.

@[simp]

theorem TopRep.gradedResolutionProjection_lof_succ {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [h : DecidableEq ℕ] (n : ℕ) (F : ↑(X.resolutionX (n + 1 + 1))) : X.gradedResolutionProjection ((DirectSum.lof R ℕ (fun (n : ℕ) => ↑(X.resolutionX (n + 1))) (n + 1)) F) = 0

The projection vanishes on the positive-degree terms.

@[simp]

theorem TopRep.gradedResolutionProjection_augmentation {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) (x : ↑X) : X.gradedResolutionProjection (X.gradedResolutionAugmentation x) = x

The projection retracts the augmentation.

noncomputable def TopRep.gradedResolutionHomotopy {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : X.gradedResolutionModule →ₗ[R] X.gradedResolutionModule

The contracting homotopy of the total shifted resolution: it lowers the degree by one, evaluating the outermost variable of a positive-degree term at 1, and vanishes in degree zero. It is the total map of TopRep.resolutionModuleHomotopy, and it is not equivariant.

@[simp]

theorem TopRep.gradedResolutionHomotopy_lof_zero {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DecidableEq ℕ] (F : ↑(X.resolutionX 1)) : X.gradedResolutionHomotopy ((DirectSum.lof R ℕ (fun (n : ℕ) => ↑(X.resolutionX (n + 1))) 0) F) = 0

The contracting homotopy vanishes in degree zero.

@[simp]

theorem TopRep.gradedResolutionHomotopy_lof_succ {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DecidableEq ℕ] (n : ℕ) (F : ↑(X.resolutionX (n + 1 + 1))) : X.gradedResolutionHomotopy ((DirectSum.lof R ℕ (fun (n : ℕ) => ↑(X.resolutionX (n + 1))) (n + 1)) F) = (DirectSum.lof R ℕ (fun (n : ℕ) => ↑(X.resolutionX (n + 1))) n) (F 1)

In positive degree, the contracting homotopy evaluates the outermost variable at 1.

@[simp]

theorem TopRep.gradedResolutionHomotopy_augmentation {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) (x : ↑X) : X.gradedResolutionHomotopy (X.gradedResolutionAugmentation x) = 0

The contracting homotopy vanishes on the augmentation.

@[simp]

theorem TopRep.gradedResolutionProjection_differential {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) (x : X.gradedResolutionModule) : X.gradedResolutionProjection (X.gradedResolutionDifferential x) = 0

The projection vanishes on the image of the total differential.

theorem TopRep.gradedResolutionDifferential_gradedResolutionHomotopy_add {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) (x : X.gradedResolutionModule) : X.gradedResolutionDifferential (X.gradedResolutionHomotopy x) + X.gradedResolutionHomotopy (X.gradedResolutionDifferential x) = x - X.gradedResolutionAugmentation (X.gradedResolutionProjection x)

The contraction identity of the total shifted resolution: d ∘ h + h ∘ d = 1 - ι ∘ π, for the augmentation ι and the projection π.

theorem TopRep.isHomogeneous_gradedResolutionHomotopy {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : TauCeti.LinearMap.IsHomogeneous X.gradedResolutionHomotopy X.gradedResolutionPiece X.gradedResolutionPiece (-1)

The contracting homotopy of the total shifted resolution has degree minus one.

theorem TopRep.gradedResolutionProjection_eq_zero_of_mem {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) {p : ℤ} (hp : p ≠ 0) {v : X.gradedResolutionModule} (hv : v ∈ X.gradedResolutionPiece p) : X.gradedResolutionProjection v = 0

The projection vanishes on every homogeneous piece of nonzero degree.

theorem TopRep.gradedResolutionHomotopy_eq_zero_of_mem_zero {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) {v : X.gradedResolutionModule} (hv : v ∈ X.gradedResolutionPiece 0) : X.gradedResolutionHomotopy v = 0

The contracting homotopy vanishes on the homogeneous piece of degree zero.

theorem TopRep.gradedResolutionProjection_map {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) {Y : TopRep R H} (f : res (↑φ) X ⟶ Y) (x : X.gradedResolutionModule) : Y.gradedResolutionProjection ((gradedResolutionMap φ f) x) = (Hom.hom f) (X.gradedResolutionProjection x)

The projection is natural in compatible pairs: evaluation at 1 commutes with F ↦ f ∘ F ∘ φ because φ 1 = 1.

theorem TopRep.gradedResolutionHomotopy_map {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) {Y : TopRep R H} (f : res (↑φ) X ⟶ Y) (x : X.gradedResolutionModule) : Y.gradedResolutionHomotopy ((gradedResolutionMap φ f) x) = (gradedResolutionMap φ f) (X.gradedResolutionHomotopy x)

The contracting homotopy is natural in compatible pairs: evaluating the outermost variable at 1 commutes with F ↦ f ∘ F ∘ φ because φ 1 = 1.

noncomputable def TopRep.gradedResolutionTopRep {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DiscreteTopology R] : TopRep R G

The total resolution with its discrete topology and componentwise group action.

@[simp]

theorem TopRep.gradedResolutionTopRep_V {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DiscreteTopology R] : ↑X.gradedResolutionTopRep = X.gradedResolutionModule

The bundled discrete representation retains the total resolution carrier.

theorem TopRep.gradedResolutionTopRep_ρ_apply {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DiscreteTopology R] (g : G) (x : X.gradedResolutionModule) : (X.gradedResolutionTopRep.ρ g) x = (X.gradedResolutionRepresentation g) x

The bundled action is the componentwise resolution action.

theorem TopRep.gradedResolutionTopRep_ρ_lof {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DiscreteTopology R] [DecidableEq ℕ] (n : ℕ) (g : G) (x : ↑(X.resolutionX (n + 1))) : (X.gradedResolutionTopRep.ρ g) ((DirectSum.lof R ℕ (fun (n : ℕ) => ↑(X.resolutionX (n + 1))) n) x) = (DirectSum.lof R ℕ (fun (n : ℕ) => ↑(X.resolutionX (n + 1))) n) (((X.resolutionX (n + 1)).ρ g) x)

The bundled discrete action on an included term is the original resolution action.

theorem TopRep.gradedResolutionTopRep_ρ_mem {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DiscreteTopology R] (n : ℤ) (g : G) (x : X.gradedResolutionModule) (hx : x ∈ X.gradedResolutionPiece n) : (X.gradedResolutionTopRep.ρ g) x ∈ X.gradedResolutionPiece n

The bundled discrete action preserves the homogeneous pieces.

instance TopRep.instDiscreteTopologyVGradedResolutionTopRep {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DiscreteTopology R] : DiscreteTopology ↑X.gradedResolutionTopRep

The total resolution carries the discrete topology.

noncomputable def TopRep.gradedResolutionTopRepDifferential {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DiscreteTopology R] : X.gradedResolutionTopRep ⟶ X.gradedResolutionTopRep

The total resolution differential as a morphism of discrete topological representations.

theorem TopRep.gradedResolutionTopRepDifferential_apply {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DiscreteTopology R] (x : X.gradedResolutionModule) : (Hom.hom X.gradedResolutionTopRepDifferential) x = X.gradedResolutionDifferential x

Bundling the total differential preserves its action on the original direct-sum carrier.

theorem TopRep.isHomogeneous_gradedResolutionTopRepDifferential {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DiscreteTopology R] : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom X.gradedResolutionTopRepDifferential).toContinuousLinearMap) X.gradedResolutionPiece X.gradedResolutionPiece 1

The bundled total differential has degree one.

@[simp]

theorem TopRep.gradedResolutionTopRepDifferential_sq {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DiscreteTopology R] : CategoryTheory.CategoryStruct.comp X.gradedResolutionTopRepDifferential X.gradedResolutionTopRepDifferential = 0

The differential of the bundled discrete resolution squares to zero.

noncomputable def TopRep.gradedResolutionTopRepAugmentation {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DiscreteTopology R] [DiscreteTopology ↑X] : X ⟶ X.gradedResolutionTopRep

The augmentation from discrete coefficients into the total resolution as a morphism of topological representations.

theorem TopRep.gradedResolutionTopRepAugmentation_apply {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DiscreteTopology R] [DiscreteTopology ↑X] (x : ↑X) : (Hom.hom X.gradedResolutionTopRepAugmentation) x = X.gradedResolutionAugmentation x

Bundling the augmentation preserves its action on the original coefficient carrier.

theorem TopRep.gradedResolutionTopRepDifferential_augmentation {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DiscreteTopology R] [DiscreteTopology ↑X] : CategoryTheory.CategoryStruct.comp X.gradedResolutionTopRepAugmentation X.gradedResolutionTopRepDifferential = 0

The bundled augmentation takes values in the kernel of the total differential.

noncomputable def TopRep.gradedResolutionTopRepResMap {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} [DiscreteTopology R] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) {Y' : TopRep R H} (f : res (↑φ) X ⟶ Y') : res (↑φ) X.gradedResolutionTopRep ⟶ Y'.gradedResolutionTopRep

Change of group on the total resolution. A compatible pair, a continuous homomorphism φ : H →ₜ* G and a morphism f : res φ X ⟶ Y', induces a morphism from the restriction along φ of the discrete total resolution of X to that of Y', given by F ↦ f ∘ F ∘ φ in every degree. It has degree zero and commutes with the differentials and the augmentations.

theorem TopRep.gradedResolutionTopRepResMap_apply {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} [DiscreteTopology R] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) {Y' : TopRep R H} (f : res (↑φ) X ⟶ Y') (x : X.gradedResolutionModule) : (Hom.hom (gradedResolutionTopRepResMap φ f)) x = (gradedResolutionMap φ f) x

The change-of-group morphism acts on the total resolution by gradedResolutionMap.

theorem TopRep.isHomogeneous_gradedResolutionTopRepResMap {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} [DiscreteTopology R] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) {Y' : TopRep R H} (f : res (↑φ) X ⟶ Y') : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom (gradedResolutionTopRepResMap φ f)).toContinuousLinearMap) X.gradedResolutionPiece Y'.gradedResolutionPiece 0

The change-of-group morphism preserves the homogeneous degrees of the total resolutions.

theorem TopRep.gradedResolutionTopRepResMap_differential {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} [DiscreteTopology R] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) {Y' : TopRep R H} (f : res (↑φ) X ⟶ Y') : CategoryTheory.CategoryStruct.comp ((resFunctor ↑φ).map X.gradedResolutionTopRepDifferential) (gradedResolutionTopRepResMap φ f) = CategoryTheory.CategoryStruct.comp (gradedResolutionTopRepResMap φ f) Y'.gradedResolutionTopRepDifferential

The change-of-group morphism commutes with the total differentials.

theorem TopRep.gradedResolutionTopRepResMap_augmentation {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} [DiscreteTopology R] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) {Y' : TopRep R H} [DiscreteTopology ↑X] [DiscreteTopology ↑Y'] (f : res (↑φ) X ⟶ Y') : CategoryTheory.CategoryStruct.comp ((resFunctor ↑φ).map X.gradedResolutionTopRepAugmentation) (gradedResolutionTopRepResMap φ f) = CategoryTheory.CategoryStruct.comp f Y'.gradedResolutionTopRepAugmentation

The change-of-group morphism lies over f: it carries the augmentation of the restricted coefficients to the augmentation of Y'.

theorem TopRep.gradedResolutionTopRepResMap_comp {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} [DiscreteTopology R] {H K : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [Group K] [TopologicalSpace K] [IsTopologicalGroup K] (φ : H →ₜ* G) {Y' : TopRep R H} (ψ : K →ₜ* H) {Z' : TopRep R K} (f : res (↑φ) X ⟶ Y') (g : res (↑ψ) Y' ⟶ Z') : gradedResolutionTopRepResMap (φ.comp ψ) (CategoryTheory.CategoryStruct.comp ((resFunctor ↑ψ).map f) g) = CategoryTheory.CategoryStruct.comp ((resFunctor ↑ψ).map (gradedResolutionTopRepResMap φ f)) (gradedResolutionTopRepResMap ψ g)

Change-of-group morphisms of total resolutions compose along composite compatible pairs.

noncomputable def TopRep.gradedResolutionTopRepMap {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} [DiscreteTopology R] {Y : TopRep R G} (f : X ⟶ Y) : X.gradedResolutionTopRep ⟶ Y.gradedResolutionTopRep

A coefficient morphism induces a morphism of discrete total resolutions.

theorem TopRep.gradedResolutionTopRepMap_apply {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} [DiscreteTopology R] {Y : TopRep R G} (f : X ⟶ Y) (x : X.gradedResolutionModule) : (Hom.hom (gradedResolutionTopRepMap f)) x = (gradedResolutionMap (ContinuousMonoidHom.id G) f) x

Bundling a coefficient map preserves its action on the original direct-sum carrier.

@[simp]

theorem TopRep.gradedResolutionTopRepMap_id {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} [DiscreteTopology R] : gradedResolutionTopRepMap (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id X.gradedResolutionTopRep

Identity coefficients induce the identity morphism of the discrete total resolution.

@[simp]

theorem TopRep.gradedResolutionTopRepMap_comp {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} [DiscreteTopology R] {Y Z : TopRep R G} (f : X ⟶ Y) (g : Y ⟶ Z) : gradedResolutionTopRepMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (gradedResolutionTopRepMap f) (gradedResolutionTopRepMap g)

Bundled coefficient maps preserve composition.

theorem TopRep.gradedResolutionTopRepMap_differential {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} [DiscreteTopology R] {Y : TopRep R G} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp X.gradedResolutionTopRepDifferential (gradedResolutionTopRepMap f) = CategoryTheory.CategoryStruct.comp (gradedResolutionTopRepMap f) Y.gradedResolutionTopRepDifferential

Bundled coefficient maps commute with the resolution differential.

theorem TopRep.gradedResolutionTopRepMap_augmentation {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} [DiscreteTopology R] {Y : TopRep R G} [DiscreteTopology ↑X] [DiscreteTopology ↑Y] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp X.gradedResolutionTopRepAugmentation (gradedResolutionTopRepMap f) = CategoryTheory.CategoryStruct.comp f Y.gradedResolutionTopRepAugmentation

Bundled coefficient maps preserve the augmentations of discrete coefficients.

theorem TopRep.isSmoothDiscrete_gradedResolutionTopRep {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DiscreteTopology R] [CompactSpace G] (hX : TauCeti.IsSmoothDiscrete R X) : TauCeti.IsSmoothDiscrete R X.gradedResolutionTopRep

For a compact group, a discrete scalar ring R, and smooth discrete coefficients, the total coinduced resolution is smooth: each element has finitely many components, whose open stabilizers have open intersection.

noncomputable def TauCeti.smoothGradedResolutionFunctor {R : Type u} [Ring R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] : CategoryTheory.Functor (SmoothDiscreteTopRep R G) (SmoothDiscreteTopRep R G)

The total shifted coinduced resolution, as a functor on smooth discrete coefficient representations.

theorem TauCeti.smoothGradedResolutionFunctor_obj {R : Type u} [Ring R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : SmoothDiscreteTopRep R G) : smoothGradedResolutionFunctor.obj A = { obj := A.obj.gradedResolutionTopRep, property := ⋯ }

The smooth total-resolution functor sends a coefficient object to its total shifted coinduced resolution.

This is not a simp lemma: rewriting the objects would take the morphism-evaluation lemmas, such as smoothGradedResolutionAugmentationApp_hom_apply, out of simp-normal form.

@[simp]

theorem TauCeti.smoothGradedResolutionFunctor_obj_obj_ρ_apply {R : Type u} [Ring R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : SmoothDiscreteTopRep R G) (g : G) (x : ↑(smoothGradedResolutionFunctor.obj A).obj) : ((smoothGradedResolutionFunctor.obj A).obj.ρ g) x = (A.obj.gradedResolutionTopRep.ρ g) x

The action on the object of the smooth total-resolution functor is the action on the total shifted coinduced resolution.

@[simp]

theorem TauCeti.smoothGradedResolutionFunctor_map {R : Type u} [Ring R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {A B : SmoothDiscreteTopRep R G} (f : A ⟶ B) : smoothGradedResolutionFunctor.map f = CategoryTheory.ObjectProperty.homMk (TopRep.gradedResolutionTopRepMap f.hom)

The smooth total-resolution functor acts on morphisms by the induced map of total resolutions.

noncomputable def TauCeti.smoothGradedResolutionAugmentationApp {R : Type u} [Ring R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : SmoothDiscreteTopRep R G) : A ⟶ smoothGradedResolutionFunctor.obj A

The coefficient augmentation into the total shifted coinduced resolution.

noncomputable def TauCeti.smoothGradedResolutionAugmentation {R : Type u} [Ring R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] : CategoryTheory.Functor.id (SmoothDiscreteTopRep R G) ⟶ smoothGradedResolutionFunctor

The coefficient augmentations into the total shifted coinduced resolution are natural among smooth discrete coefficient representations.

@[simp]

theorem TauCeti.smoothGradedResolutionAugmentation_app {R : Type u} [Ring R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : SmoothDiscreteTopRep R G) : smoothGradedResolutionAugmentation.app A = smoothGradedResolutionAugmentationApp A

The component of the smooth total-resolution augmentation is the named augmentation.

@[simp]

theorem TauCeti.smoothGradedResolutionAugmentationApp_hom_apply {R : Type u} [Ring R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : SmoothDiscreteTopRep R G) (x : ↑A.obj) : (TopRep.Hom.hom (smoothGradedResolutionAugmentationApp A).hom) x = A.obj.gradedResolutionAugmentation x

The smooth total-resolution augmentation acts by the ordinary augmentation on carriers.

noncomputable def TauCeti.smoothGradedResolutionDifferential {R : Type u} [Ring R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : SmoothDiscreteTopRep R G) : smoothGradedResolutionFunctor.obj A ⟶ smoothGradedResolutionFunctor.obj A

The differential of the total shifted coinduced resolution, as an endomorphism of the smooth total resolution.

@[simp]

theorem TauCeti.smoothGradedResolutionDifferential_hom_apply {R : Type u} [Ring R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (A : SmoothDiscreteTopRep R G) (x : A.obj.gradedResolutionModule) : (TopRep.Hom.hom (smoothGradedResolutionDifferential A).hom) x = A.obj.gradedResolutionDifferential x

The smooth total-resolution differential acts by the ordinary total differential on carriers.

noncomputable def TauCeti.smoothGradedResolutionResMap {R : Type u} [Ring R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] (φ : H →* G) (hφ : Continuous ⇑φ) (A : SmoothDiscreteTopRep R G) : (smoothResFunctor R φ hφ).obj (smoothGradedResolutionFunctor.obj A) ⟶ smoothGradedResolutionFunctor.obj ((smoothResFunctor R φ hφ).obj A)

Restriction of the smooth total resolution. The restriction along a continuous homomorphism φ : H →* G of the total resolution of A, compared with the total resolution of the restriction of A: it pulls back cochains along φ (TopRep.gradedResolutionTopRepResMap).

theorem TauCeti.smoothGradedResolutionResMap_hom_hom_apply {R : Type u} [Ring R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] (φ : H →* G) (hφ : Continuous ⇑φ) (A : SmoothDiscreteTopRep R G) (x : A.obj.gradedResolutionModule) : (TopRep.Hom.hom (smoothGradedResolutionResMap φ hφ A).hom) x = (TopRep.gradedResolutionMap { toMonoidHom := φ, continuous_toFun := hφ } (CategoryTheory.CategoryStruct.id (TopRep.res (↑{ toMonoidHom := φ, continuous_toFun := hφ }) A.obj))) x

The restriction of the smooth total resolution pulls back cochains along φ.

theorem TauCeti.isHomogeneous_smoothGradedResolutionResMap {R : Type u} [Ring R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] (φ : H →* G) (hφ : Continuous ⇑φ) (A : SmoothDiscreteTopRep R G) : LinearMap.IsHomogeneous (↑(TopRep.Hom.hom (smoothGradedResolutionResMap φ hφ A).hom).toContinuousLinearMap) A.obj.gradedResolutionPiece ((smoothResFunctor R φ hφ).obj A).obj.gradedResolutionPiece 0

The restriction of the smooth total resolution preserves degrees.

theorem TauCeti.smoothGradedResolutionResMap_differential {R : Type u} [Ring R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] (φ : H →* G) (hφ : Continuous ⇑φ) (A : SmoothDiscreteTopRep R G) (x : A.obj.gradedResolutionModule) : (TopRep.Hom.hom (smoothGradedResolutionResMap φ hφ A).hom) (A.obj.gradedResolutionDifferential x) = ((smoothResFunctor R φ hφ).obj A).obj.gradedResolutionDifferential ((TopRep.Hom.hom (smoothGradedResolutionResMap φ hφ A).hom) x)

The restriction of the smooth total resolution commutes with the total differentials.

@[simp]

theorem TauCeti.smoothGradedResolutionResMap_augmentation {R : Type u} [Ring R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] (φ : H →* G) (hφ : Continuous ⇑φ) (A : SmoothDiscreteTopRep R G) (x : ↑A.obj) : (TopRep.Hom.hom (smoothGradedResolutionResMap φ hφ A).hom) (A.obj.gradedResolutionAugmentation x) = ((smoothResFunctor R φ hφ).obj A).obj.gradedResolutionAugmentation x

The restriction of the smooth total resolution commutes with the augmentations.