Tensor induction of the total coinduced resolution

Let U be a compact open finite-index subgroup of a topological group G, and let A be a smooth discrete U-representation. The shifted coinduced resolution of A has a smooth discrete total object, so it can itself be tensor-induced from U to G. This file names that object and its augmentation from the tensor induction of A.

On a pure tensor, the augmentation applies the ordinary coinduced-resolution augmentation in every coset coordinate, and the construction is natural in A. Compatibility with changing the transversal is the naturality of TauCeti.smoothTensorInducedChangeTransversalIso, applied to the components of the augmentation.

When every element of A is its own additive inverse, the tensor-induced total resolution is a contracted complex, on which Evens' multiplicative transfer is computed. It is graded by total degree, and its differential is the slot sum of the total differential, which applies it in one coset factor at a time; it commutes with the action of G because the slot sum needs no signs and so commutes with permuting the factors. The tensor power of the contraction of the total resolution by evaluation at 1, with the slot homotopy for an order on the cosets, contracts it onto the tensor induction of A (TauCeti.smoothTensorInducedGradedResolutionContraction).

For a U-invariant cocycle z of degree n of the total resolution of A, the diagonal tensor z ⊗ ⋯ ⊗ z, with one factor for each of the l cosets, is a G-invariant cocycle of degree l * n. Its class TauCeti.smoothTensorInducedDiagonalClass in H^{l n}(G, Ind⊗ A) is the norm of z in the sense of Evens; it does not depend on the order on the cosets used to contract the resolution. It is invariant under chain endomorphisms of the total resolution over the identity of A, since their tensor inductions are chain maps over the identity of Ind⊗ A. The norm is not additive, but over a coefficient ring in which 2 generates a maximal ideal, such as ℤ for trivial 𝔽₂ coefficients, such an endomorphism moves a nonzero cocycle z to z + d w for any invariant w, so cohomologous cocycles have the same norm.

The tensor-induced resolution and the total resolution of Ind⊗ A are both contracted onto Ind⊗ A, so the comparison theorem gives a morphism of degree zero between them over the identity (TauCeti.smoothTensorInducedGradedResolutionComparison). It carries the diagonal tensor of z to a cocycle of the total resolution whose class is the norm of z, which is the form in which a norm is the input of a further norm.

Main definitions

• TauCeti.smoothTensorInducedGradedResolutionFunctor: tensor induction of the total shifted coinduced resolution, functorially in the coefficients.
• TauCeti.smoothTensorInducedGradedResolutionAugmentationApp: the tensor-induced augmentation of a single coefficient object.
• TauCeti.smoothTensorInducedGradedResolutionAugmentation: the natural tensor-induced augmentation.
• TauCeti.smoothTensorInducedGradedResolutionPiece and TauCeti.smoothTensorInducedGradedResolutionDifferential: the total-degree grading and the slot-sum differential of the tensor-induced total resolution.
• TauCeti.smoothTensorInducedGradedResolutionContraction: its contraction onto the tensor induction of the coefficients, in characteristic two.
• TauCeti.smoothTensorInducedDiagonalClass: the class in H^{l n}(G, Ind⊗ A) of the diagonal tensor of a U-invariant cocycle of degree n.
• TauCeti.smoothTensorInducedGradedResolutionComparison: the comparison of the tensor-induced resolution with the total resolution of the tensor-induced coefficients.

Main results

• TauCeti.smoothTensorInducedGradedResolutionDifferential_sq: in characteristic two the differential squares to zero.
• TauCeti.slotSum_smoothTensorInducedGradedResolutionHomotopy_add: the contraction identity.
• TauCeti.smoothTensorInducedDiagonalClass_eq: the class of the diagonal tensor does not depend on the order on the cosets: it equals the class computed through the contraction for any order.
• TauCeti.gradedCohomologyClass_smoothTensorInducedGradedResolutionComparison: the comparison carries the diagonal tensor of a cocycle to a cocycle of the total resolution representing its norm.
• TauCeti.smoothTensorInducedDiagonalClass_eq_of_hom_apply_eq: the norm is invariant under chain endomorphisms of the total resolution over the identity of the coefficients.
• TauCeti.smoothTensorInducedDiagonalClass_eq_of_sub_eq_d: cohomologous cocycles have the same norm, when 2 generates a maximal ideal of the coefficient ring.
• Subgroup.smoothTensorInducedDiagonalClass_eq_degreeZeroClass: in degree zero the norm of a cocycle with value a is the degree-zero class of the invariant tensor a ⊗ ⋯ ⊗ a.

References

• L. Evens, A generalization of the transfer map in the cohomology of groups, Transactions of the American Mathematical Society 108 (1963), Sections 2--5.

noncomputable def TauCeti.smoothTensorInducedGradedResolutionFunctor {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] : CategoryTheory.Functor (SmoothDiscreteTopRep R ↥U) (SmoothDiscreteTopRep R G)

Tensor induction from U to G of the total shifted coinduced resolution, functorially in the smooth discrete coefficient object.

theorem TauCeti.smoothTensorInducedGradedResolutionFunctor_obj {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) : (smoothTensorInducedGradedResolutionFunctor U hU s).obj A = (smoothTensorInductionFunctor R G U hU s).obj (smoothGradedResolutionFunctor.obj A)

The object map of the tensor-induced total resolution tensor-induces the total resolution of the coefficient object.

This is not a simp lemma: rewriting the objects would take the pure-tensor evaluation lemma smoothTensorInducedGradedResolutionAugmentationApp_apply_tprod out of simp-normal form.

@[simp]

theorem TauCeti.smoothTensorInducedGradedResolutionFunctor_map {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] {A B : SmoothDiscreteTopRep R ↥U} (f : A ⟶ B) : (smoothTensorInducedGradedResolutionFunctor U hU s).map f = (smoothTensorInductionFunctor R G U hU s).map (smoothGradedResolutionFunctor.map f)

The morphism map of the tensor-induced total resolution tensor-induces the induced map of total resolutions.

theorem Subgroup.smoothTensorInducedGradedResolutionFunctor_map_hom_hom_apply {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] {A B : TauCeti.SmoothDiscreteTopRep R ↥U} (f : A ⟶ B) (x : PiTensorProduct R fun (x : G ⧸ U) => A.obj.gradedResolutionModule) : (TopRep.Hom.hom ((TauCeti.smoothTensorInducedGradedResolutionFunctor U hU s).map f).hom) x = (PiTensorProduct.map fun (x : G ⧸ U) => TopRep.gradedResolutionMap (ContinuousMonoidHom.id ↥U) f.hom) x

On carriers, the induced morphism of tensor-induced total resolutions applies the total resolution map in each tensor factor.

@[simp]

theorem Subgroup.smoothTensorInducedGradedResolutionFunctor_map_hom_hom_apply_tprod {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] {A B : TauCeti.SmoothDiscreteTopRep R ↥U} (f : A ⟶ B) (x : G ⧸ U → A.obj.gradedResolutionModule) : (TopRep.Hom.hom ((TauCeti.smoothTensorInducedGradedResolutionFunctor U hU s).map f).hom) ((PiTensorProduct.tprod R) x) = (PiTensorProduct.tprod R) fun (i : G ⧸ U) => (TopRep.gradedResolutionMap (ContinuousMonoidHom.id ↥U) f.hom) (x i)

On a pure tensor, the induced morphism applies the total resolution map in each coset coordinate.

theorem TauCeti.smoothTensorInducedGradedResolutionFunctor_obj_ρ_apply {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) (g : G) (x : ↑((smoothTensorInducedGradedResolutionFunctor U hU s).obj A).obj) : (((smoothTensorInducedGradedResolutionFunctor U hU s).obj A).obj.ρ g) x = ((U.tensorInducedRepresentation s ((ofSmoothDiscrete R ↥U).obj (smoothGradedResolutionFunctor.obj A)).ρ) g) x

The action of G on the tensor-induced total resolution is tensor induction of the action of U on the total resolution.

theorem TauCeti.smoothTensorInducedGradedResolutionFunctor_obj_ρ_apply' {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) (g : G) (x : ↑((smoothTensorInducedGradedResolutionFunctor U hU s).obj A).obj) : (((smoothTensorInducedGradedResolutionFunctor U hU s).obj A).obj.ρ g) x = ((U.tensorInducedRepresentation s A.obj.gradedResolutionRepresentation) g) x

The action of G on the tensor-induced total resolution is tensor induction of the action TopRep.gradedResolutionRepresentation of U on the total resolution, with no passage through the smooth-discrete dictionary.

noncomputable def TauCeti.smoothTensorInducedGradedResolutionAugmentationApp {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) : (toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj A)) ⟶ (smoothTensorInducedGradedResolutionFunctor U hU s).obj A

Tensor induction of the coefficient augmentation into the total shifted coinduced resolution.

The source is written in the simp-normal form produced by smoothTensorInductionFunctor_obj, so that the pure-tensor computation rule below can be a simp lemma.

@[simp]

theorem TauCeti.smoothTensorInducedGradedResolutionAugmentationApp_apply_tprod {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) (x : G ⧸ U → ↑A.obj) : (TopRep.Hom.hom (smoothTensorInducedGradedResolutionAugmentationApp U hU s A).hom) ((PiTensorProduct.tprod R) x) = (PiTensorProduct.tprod R) fun (i : G ⧸ U) => A.obj.gradedResolutionAugmentation (x i)

On a pure tensor, the tensor-induced augmentation applies the coinduced-resolution augmentation in every coset coordinate.

noncomputable def TauCeti.smoothTensorInducedGradedResolutionAugmentation {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] : smoothTensorInductionFunctor R G U hU s ⟶ smoothTensorInducedGradedResolutionFunctor U hU s

The tensor-induced coefficient augmentations, as a natural transformation into the tensor-induced total resolution: the right whiskering of smoothGradedResolutionAugmentation by smooth tensor induction.

@[simp]

theorem TauCeti.smoothTensorInducedGradedResolutionAugmentation_app {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) : (smoothTensorInducedGradedResolutionAugmentation U hU s).app A = smoothTensorInducedGradedResolutionAugmentationApp U hU s A

The component of the tensor-induced augmentation is the named tensor-induced augmentation.

theorem TauCeti.smoothTensorInducedGradedResolutionAugmentationApp_hom_apply {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) (x : PiTensorProduct R fun (x : G ⧸ U) => ↑A.obj) : (TopRep.Hom.hom (smoothTensorInducedGradedResolutionAugmentationApp U hU s A).hom) x = (PiTensorProduct.map fun (x : G ⧸ U) => A.obj.gradedResolutionAugmentation) x

The tensor-induced augmentation applies the coinduced-resolution augmentation in every coset factor.

This is not a simp lemma, so that smoothTensorInducedGradedResolutionAugmentationApp_apply_tprod still evaluates the augmentation on pure tensors.

The contracted tensor-induced resolution

@[reducible, inline]

noncomputable abbrev TauCeti.smoothTensorInducedGradedResolutionPiece {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] : ℤ → Submodule R ↑((smoothTensorInducedGradedResolutionFunctor U hU s).obj A).obj

The total-degree grading of the tensor-induced total resolution: a pure tensor of homogeneous factors has the sum of their degrees.

@[instance_reducible]

noncomputable instance TauCeti.smoothTensorInducedGradedResolutionPieceDecomposition {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] : DirectSum.Decomposition (smoothTensorInducedGradedResolutionPiece U hU s A)

The total-degree pieces decompose the tensor-induced resolution. Thus a degreewise comparison out of this resolution assembles into a map on its whole underlying module.

theorem TauCeti.smoothTensorInducedGradedResolutionPiece_ρ_mem {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] (n : ℤ) (g : G) (x : ↑((smoothTensorInducedGradedResolutionFunctor U hU s).obj A).obj) (hx : x ∈ smoothTensorInducedGradedResolutionPiece U hU s A n) : (((smoothTensorInducedGradedResolutionFunctor U hU s).obj A).obj.ρ g) x ∈ smoothTensorInducedGradedResolutionPiece U hU s A n

The action of G on the tensor-induced total resolution preserves the total degree.

noncomputable def TauCeti.smoothTensorInducedGradedResolutionDifferential {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] : (smoothTensorInducedGradedResolutionFunctor U hU s).obj A ⟶ (smoothTensorInducedGradedResolutionFunctor U hU s).obj A

The differential of the tensor-induced total resolution: the slot sum of the total differential, which applies it in one coset factor at a time. It is a complex in characteristic two (TauCeti.smoothTensorInducedGradedResolutionDifferential_sq).

@[simp]

theorem TauCeti.smoothTensorInducedGradedResolutionDifferential_apply {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] [DecidableEq (G ⧸ U)] (z : ↑((smoothTensorInducedGradedResolutionFunctor U hU s).obj A).obj) : (TopRep.Hom.hom (smoothTensorInducedGradedResolutionDifferential U hU s A).hom) z = (PiTensorProduct.slotSum (G ⧸ U) fun (x : G ⧸ U) => A.obj.gradedResolutionDifferential) z

The differential of the tensor-induced total resolution is the slot sum of the total differential.

theorem TauCeti.isHomogeneous_smoothTensorInducedGradedResolutionDifferential {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] : LinearMap.IsHomogeneous (↑(TopRep.Hom.hom (smoothTensorInducedGradedResolutionDifferential U hU s A).hom).toContinuousLinearMap) (smoothTensorInducedGradedResolutionPiece U hU s A) (smoothTensorInducedGradedResolutionPiece U hU s A) 1

The differential of the tensor-induced total resolution raises the total degree by one.

theorem TauCeti.smoothTensorInducedGradedResolutionDifferential_sq {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] (hA : ∀ (a : ↑A.obj), a + a = 0) : CategoryTheory.CategoryStruct.comp (smoothTensorInducedGradedResolutionDifferential U hU s A).hom (smoothTensorInducedGradedResolutionDifferential U hU s A).hom = 0

The tensor-induced total resolution is a complex in characteristic two: if every coefficient is its own additive inverse, its differential squares to zero. Applying the total differential in two distinct coset factors gives the same term in either order, and these terms cancel in pairs.

noncomputable def TauCeti.smoothTensorInducedGradedResolutionProjection {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (A : SmoothDiscreteTopRep R ↥U) : (PiTensorProduct R fun (x : G ⧸ U) => A.obj.gradedResolutionModule) →ₗ[R] PiTensorProduct R fun (x : G ⧸ U) => ↑A.obj

The projection of the tensor-induced total resolution onto the tensor induction of the coefficients: the projection of the total resolution, evaluation at 1 in degree zero, in every coset factor. It is not equivariant.

theorem TauCeti.smoothTensorInducedGradedResolutionProjection_def {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (A : SmoothDiscreteTopRep R ↥U) : smoothTensorInducedGradedResolutionProjection U A = PiTensorProduct.map fun (x : G ⧸ U) => A.obj.gradedResolutionProjection

The projection of the tensor-induced total resolution is the projection of the total resolution in every coset factor.

@[simp]

theorem TauCeti.smoothTensorInducedGradedResolutionProjection_tprod {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (A : SmoothDiscreteTopRep R ↥U) (m : G ⧸ U → A.obj.gradedResolutionModule) : (smoothTensorInducedGradedResolutionProjection U A) ((PiTensorProduct.tprod R) m) = (PiTensorProduct.tprod R) fun (i : G ⧸ U) => A.obj.gradedResolutionProjection (m i)

On a pure tensor, the projection applies the projection of the total resolution in every coset factor.

theorem TauCeti.smoothTensorInducedGradedResolutionProjection_augmentation {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (A : SmoothDiscreteTopRep R ↥U) (x : PiTensorProduct R fun (x : G ⧸ U) => ↑A.obj) : (smoothTensorInducedGradedResolutionProjection U A) ((PiTensorProduct.map fun (x : G ⧸ U) => A.obj.gradedResolutionAugmentation) x) = x

The projection retracts the tensor-induced augmentation.

theorem TauCeti.smoothTensorInducedGradedResolutionAugmentationApp_mem {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] (x : ↑((toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj A))).obj) : (TopRep.Hom.hom (smoothTensorInducedGradedResolutionAugmentationApp U hU s A).hom) x ∈ smoothTensorInducedGradedResolutionPiece U hU s A 0

The tensor-induced augmentation lands in total degree zero.

noncomputable def TauCeti.smoothTensorInducedGradedResolutionHomotopy {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] [LinearOrder (G ⧸ U)] : Module.End R (PiTensorProduct R fun (x : G ⧸ U) => A.obj.gradedResolutionModule)

The contracting homotopy of the tensor-induced total resolution, for an order on the cosets: the slot homotopy applying the projection followed by the augmentation in the factors before a slot, the contracting homotopy of the total resolution at the slot, and the identity after it. It lowers the total degree by one and is not equivariant.

theorem TauCeti.smoothTensorInducedGradedResolutionHomotopy_def {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] [LinearOrder (G ⧸ U)] : smoothTensorInducedGradedResolutionHomotopy U A = PiTensorProduct.slotHomotopy (G ⧸ U) (fun (x : G ⧸ U) => A.obj.gradedResolutionAugmentation ∘ₗ A.obj.gradedResolutionProjection) fun (x : G ⧸ U) => A.obj.gradedResolutionHomotopy

The contracting homotopy of the tensor-induced total resolution is the slot homotopy of the projection followed by the augmentation, and of the contracting homotopy of the total resolution.

theorem TauCeti.isHomogeneous_smoothTensorInducedGradedResolutionHomotopy {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] [LinearOrder (G ⧸ U)] : LinearMap.IsHomogeneous (smoothTensorInducedGradedResolutionHomotopy U A) (PiTensorProduct.totalDegreePiece (G ⧸ U) fun (x : G ⧸ U) => A.obj.gradedResolutionPiece) (PiTensorProduct.totalDegreePiece (G ⧸ U) fun (x : G ⧸ U) => A.obj.gradedResolutionPiece) (-1)

The contracting homotopy of the tensor-induced total resolution lowers the total degree by one.

theorem TauCeti.slotSum_smoothTensorInducedGradedResolutionHomotopy_add {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] [LinearOrder (G ⧸ U)] (hA : ∀ (a : ↑A.obj), a + a = 0) (v : PiTensorProduct R fun (x : G ⧸ U) => A.obj.gradedResolutionModule) : (PiTensorProduct.slotSum (G ⧸ U) fun (x : G ⧸ U) => A.obj.gradedResolutionDifferential) ((smoothTensorInducedGradedResolutionHomotopy U A) v) + (smoothTensorInducedGradedResolutionHomotopy U A) ((PiTensorProduct.slotSum (G ⧸ U) fun (x : G ⧸ U) => A.obj.gradedResolutionDifferential) v) = v - (PiTensorProduct.map fun (x : G ⧸ U) => A.obj.gradedResolutionAugmentation) ((smoothTensorInducedGradedResolutionProjection U A) v)

The contraction identity of the tensor-induced total resolution in characteristic two: d ∘ h + h ∘ d = 1 - ι ∘ π for the slot sum d of the total differential, the contracting homotopy h, the tensor-induced augmentation ι and the projection π.

noncomputable def TauCeti.smoothTensorInducedGradedResolutionContraction {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] [LinearOrder (G ⧸ U)] (hA : ∀ (a : ↑A.obj), a + a = 0) : ((toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj A))).obj.ResolutionContraction (((smoothTensorInducedGradedResolutionFunctor U hU s).obj A).obj.gradedCochainComplex (smoothTensorInducedGradedResolutionPiece U hU s A) ⋯ (smoothTensorInducedGradedResolutionDifferential U hU s A).hom ⋯ ⋯)

The contraction of the tensor-induced total resolution onto the tensor induction of the coefficients, in characteristic two and for an order on the cosets: the tensor-induced augmentation, the projection smoothTensorInducedGradedResolutionProjection and the slot homotopy smoothTensorInducedGradedResolutionHomotopy. Through it an invariant cocycle of the tensor-induced resolution has a class in the continuous cohomology of the tensor induction.

theorem TauCeti.smoothTensorInducedGradedResolutionContraction_ι {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] [LinearOrder (G ⧸ U)] (hA : ∀ (a : ↑A.obj), a + a = 0) : (smoothTensorInducedGradedResolutionContraction U hU s A hA).ι = ((smoothTensorInducedGradedResolutionFunctor U hU s).obj A).obj.gradedCochainComplexLift (smoothTensorInducedGradedResolutionPiece U hU s A) ⋯ (smoothTensorInducedGradedResolutionDifferential U hU s A).hom ⋯ ⋯ 0 (smoothTensorInducedGradedResolutionAugmentationApp U hU s A).hom ⋯

The augmentation of the contraction of the tensor-induced total resolution is the tensor-induced augmentation; in particular it does not depend on the order on the cosets.

@[simp]

theorem TauCeti.smoothTensorInducedGradedResolutionContraction_ι_apply {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] [LinearOrder (G ⧸ U)] (hA : ∀ (a : ↑A.obj), a + a = 0) (x : ↑((toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj A))).obj) : ↑((TopRep.Hom.hom (smoothTensorInducedGradedResolutionContraction U hU s A hA).ι) x) = (PiTensorProduct.map fun (x : G ⧸ U) => A.obj.gradedResolutionAugmentation) x

The augmentation of the contraction of the tensor-induced total resolution applies the coinduced-resolution augmentation in every coset factor.

@[simp]

theorem TauCeti.smoothTensorInducedGradedResolutionContraction_proj_apply {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] [LinearOrder (G ⧸ U)] (hA : ∀ (a : ↑A.obj), a + a = 0) (v : ↑((((smoothTensorInducedGradedResolutionFunctor U hU s).obj A).obj.gradedCochainComplex (smoothTensorInducedGradedResolutionPiece U hU s A) ⋯ (smoothTensorInducedGradedResolutionDifferential U hU s A).hom ⋯ ⋯).X 0)) : (smoothTensorInducedGradedResolutionContraction U hU s A hA).proj v = (smoothTensorInducedGradedResolutionProjection U A) ↑v

The retraction of the contraction of the tensor-induced total resolution is TauCeti.smoothTensorInducedGradedResolutionProjection.

@[simp]

theorem TauCeti.smoothTensorInducedGradedResolutionContraction_hom_apply {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] [LinearOrder (G ⧸ U)] (hA : ∀ (a : ↑A.obj), a + a = 0) (n : ℕ) (v : ↑((((smoothTensorInducedGradedResolutionFunctor U hU s).obj A).obj.gradedCochainComplex (smoothTensorInducedGradedResolutionPiece U hU s A) ⋯ (smoothTensorInducedGradedResolutionDifferential U hU s A).hom ⋯ ⋯).X (n + 1))) : ↑(((smoothTensorInducedGradedResolutionContraction U hU s A hA).hom n) v) = (smoothTensorInducedGradedResolutionHomotopy U A) ↑v

The contracting homotopy of the contraction of the tensor-induced total resolution is TauCeti.smoothTensorInducedGradedResolutionHomotopy.

theorem TauCeti.tprod_const_mem_smoothTensorInducedGradedResolutionPiece {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] {n : ℕ} {z : A.obj.gradedResolutionModule} (hz : z ∈ A.obj.gradedResolutionPiece ↑n) : ((PiTensorProduct.tprod R) fun (x : G ⧸ U) => z) ∈ smoothTensorInducedGradedResolutionPiece U hU s A ↑(Fintype.card (G ⧸ U) * n)

The diagonal tensor z ⊗ ⋯ ⊗ z of a homogeneous element of degree n has total degree l * n, for l the number of cosets.

theorem TauCeti.smoothTensorInducedGradedResolutionFunctor_obj_ρ_tprod_const {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) {z : A.obj.gradedResolutionModule} (hinv : ∀ (u : ↥U), (A.obj.gradedResolutionTopRep.ρ u) z = z) (g : G) : (((smoothTensorInducedGradedResolutionFunctor U hU s).obj A).obj.ρ g) ((PiTensorProduct.tprod R) fun (x : G ⧸ U) => z) = (PiTensorProduct.tprod R) fun (x : G ⧸ U) => z

The diagonal tensor z ⊗ ⋯ ⊗ z of a U-invariant element of the total resolution is G-invariant.

theorem TauCeti.smoothTensorInducedGradedResolutionDifferential_tprod_const_eq_zero {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] {z : A.obj.gradedResolutionModule} (hdz : A.obj.gradedResolutionDifferential z = 0) : (TopRep.Hom.hom (smoothTensorInducedGradedResolutionDifferential U hU s A).hom) ((PiTensorProduct.tprod R) fun (x : G ⧸ U) => z) = 0

The diagonal tensor z ⊗ ⋯ ⊗ z of a cocycle is a cocycle: each term of the slot sum applies the differential to a factor.

noncomputable def TauCeti.smoothTensorInducedDiagonalClass {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] (hA : ∀ (a : ↑A.obj), a + a = 0) {n : ℕ} (z : A.obj.gradedResolutionModule) (hz : z ∈ A.obj.gradedResolutionPiece ↑n) (hinv : ∀ (u : ↥U), (A.obj.gradedResolutionTopRep.ρ u) z = z) (hdz : A.obj.gradedResolutionDifferential z = 0) : ↑(continuousCohomology (Fintype.card (G ⧸ U) * n) ((toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj A))).obj).toModuleCat

The Evens norm of a cocycle: for a homogeneous cocycle z of degree n of the total coinduced resolution of A, fixed by U, the class in H^{l n}(G, Ind⊗ A) of its diagonal tensor z ⊗ ⋯ ⊗ z, one factor for each of the l cosets of U. Here A has characteristic two, so that the tensor-induced resolution is a complex, and the class is computed through TauCeti.smoothTensorInducedGradedResolutionContraction for some order on the cosets; by TauCeti.smoothTensorInducedDiagonalClass_eq it does not depend on that order.

theorem TauCeti.smoothTensorInducedDiagonalClass_eq {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] [LinearOrder (G ⧸ U)] (hA : ∀ (a : ↑A.obj), a + a = 0) {n : ℕ} (z : A.obj.gradedResolutionModule) (hz : z ∈ A.obj.gradedResolutionPiece ↑n) (hinv : ∀ (u : ↥U), (A.obj.gradedResolutionTopRep.ρ u) z = z) (hdz : A.obj.gradedResolutionDifferential z = 0) : smoothTensorInducedDiagonalClass U hU s A hA z hz hinv hdz = (smoothTensorInducedGradedResolutionContraction U hU s A hA).gradedCohomologyClass ((PiTensorProduct.tprod R) fun (x : G ⧸ U) => z) ⋯ ⋯ ⋯

The norm of a cocycle does not depend on the order on the cosets: it is the class of the diagonal tensor through the contraction of the tensor-induced resolution for any order.

theorem Subgroup.smoothTensorInduced_ρ_tprod_gradedResolutionProjection {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : TauCeti.SmoothDiscreteTopRep R ↥U) {z : A.obj.gradedResolutionModule} (hz : z ∈ A.obj.gradedResolutionPiece ↑0) (hinv : ∀ (u : ↥U), (A.obj.gradedResolutionTopRep.ρ u) z = z) (hdz : A.obj.gradedResolutionDifferential z = 0) (g : G) : (((TauCeti.toSmoothDiscrete R G).obj (TauCeti.DiscreteRep.tensorInduced U hU s ((TauCeti.ofSmoothDiscrete R ↥U).obj A))).obj.ρ g) ((PiTensorProduct.tprod R) fun (x : G ⧸ U) => A.obj.gradedResolutionProjection z) = (PiTensorProduct.tprod R) fun (x : G ⧸ U) => A.obj.gradedResolutionProjection z

The diagonal tensor a ⊗ ⋯ ⊗ a of the value a = z(1) of a U-invariant degree-zero cocycle z of the total resolution is G-invariant.

theorem Subgroup.smoothTensorInducedDiagonalClass_eq_degreeZeroClass {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : TauCeti.SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] (hA : ∀ (a : ↑A.obj), a + a = 0) (z : A.obj.gradedResolutionModule) (hz : z ∈ A.obj.gradedResolutionPiece ↑0) (hinv : ∀ (u : ↥U), (A.obj.gradedResolutionTopRep.ρ u) z = z) (hdz : A.obj.gradedResolutionDifferential z = 0) : TauCeti.smoothTensorInducedDiagonalClass U hU s A hA z hz hinv hdz = TauCeti.ContinuousCohomology.degreeZeroClass ((TauCeti.toSmoothDiscrete R G).obj (TauCeti.DiscreteRep.tensorInduced U hU s ((TauCeti.ofSmoothDiscrete R ↥U).obj A))).obj ((PiTensorProduct.tprod R) fun (x : G ⧸ U) => A.obj.gradedResolutionProjection z) ⋯

The norm of a degree-zero cocycle: in degree zero the class of the diagonal tensor of a cocycle z is the degree-zero class of the diagonal tensor a ⊗ ⋯ ⊗ a of its value a = z(1) ∈ A, read through H⁰(G, Ind⊗ A) = (Ind⊗ A)^G.

theorem TauCeti.smoothTensorInducedDiagonalClass_eq_of_hom_apply_eq {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] (hA : ∀ (a : ↑A.obj), a + a = 0) {n : ℕ} {z z' : A.obj.gradedResolutionModule} (hz : z ∈ A.obj.gradedResolutionPiece ↑n) (hz' : z' ∈ A.obj.gradedResolutionPiece ↑n) (hinv : ∀ (u : ↥U), (A.obj.gradedResolutionTopRep.ρ u) z = z) (hinv' : ∀ (u : ↥U), (A.obj.gradedResolutionTopRep.ρ u) z' = z') (hdz : A.obj.gradedResolutionDifferential z = 0) (hdz' : A.obj.gradedResolutionDifferential z' = 0) (Φ : A.obj.gradedResolutionTopRep ⟶ A.obj.gradedResolutionTopRep) (hΦd : CategoryTheory.CategoryStruct.comp A.obj.gradedResolutionTopRepDifferential Φ = CategoryTheory.CategoryStruct.comp Φ A.obj.gradedResolutionTopRepDifferential) (hΦι : ∀ (x : ↑A.obj), (TopRep.Hom.hom Φ) (A.obj.gradedResolutionAugmentation x) = A.obj.gradedResolutionAugmentation x) (hΦ : LinearMap.IsHomogeneous (↑(TopRep.Hom.hom Φ).toContinuousLinearMap) A.obj.gradedResolutionPiece A.obj.gradedResolutionPiece 0) (hΦz : (TopRep.Hom.hom Φ) z = z') : smoothTensorInducedDiagonalClass U hU s A hA z' hz' hinv' hdz' = smoothTensorInducedDiagonalClass U hU s A hA z hz hinv hdz

The norm of a cocycle is invariant under chain endomorphisms over the identity. Let Φ be an endomorphism of the total resolution of A of degree zero, commuting with the differential and fixing the augmentation. Then a U-invariant cocycle z and its image Φ z have the same norm: the tensor induction of Φ carries the diagonal tensor of z to that of Φ z and is a chain map over the identity of the tensor-induced coefficients.

theorem TauCeti.smoothTensorInducedDiagonalClass_eq_of_sub_eq_d {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] [(Ideal.span {2}).IsMaximal] (hA : ∀ (a : ↑A.obj), a + a = 0) {n : ℕ} {z z' : A.obj.gradedResolutionModule} (hz : z ∈ A.obj.gradedResolutionPiece ↑(n + 1)) (hz' : z' ∈ A.obj.gradedResolutionPiece ↑(n + 1)) (hinv : ∀ (u : ↥U), (A.obj.gradedResolutionTopRep.ρ u) z = z) (hinv' : ∀ (u : ↥U), (A.obj.gradedResolutionTopRep.ρ u) z' = z') (hdz : A.obj.gradedResolutionDifferential z = 0) (hdz' : A.obj.gradedResolutionDifferential z' = 0) {y : A.obj.gradedResolutionModule} (hy : y ∈ A.obj.gradedResolutionPiece ↑n) (hyinv : ∀ (u : ↥U), (A.obj.gradedResolutionTopRep.ρ u) y = y) (hzy : z - z' = A.obj.gradedResolutionDifferential y) : smoothTensorInducedDiagonalClass U hU s A hA z hz hinv hdz = smoothTensorInducedDiagonalClass U hU s A hA z' hz' hinv' hdz'

Cohomologous cocycles have the same norm. Let R be a commutative ring in which 2 generates a maximal ideal, such as ℤ, so that A, whose elements are their own additive inverses, is a vector space over the field R ⧸ (2). If two U-invariant cocycles z and z' of the total resolution of A differ by the differential of a U-invariant element, their diagonal tensors have the same class in H^{l (n + 1)}(G, Ind⊗ A). So the norm of a cocycle depends only on its class.

Although the norm is not additive, the coboundary can be moved by a chain endomorphism of the total resolution over the identity of A (TopRep.exists_gradedResolutionTopRep_hom_apply_eq_add_of_add_self_eq_zero), under which the norm is invariant (TauCeti.smoothTensorInducedDiagonalClass_eq_of_hom_apply_eq).

The comparison with the total resolution of the tensor-induced coefficients

noncomputable def TauCeti.smoothTensorInducedGradedResolutionComparison {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] {R : Type} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] [CompactSpace G] [Fintype (G ⧸ U)] [LinearOrder (G ⧸ U)] (A : SmoothDiscreteTopRep R ↥U) (hA : ∀ (a : ↑A.obj), a + a = 0) : (smoothTensorInducedGradedResolutionFunctor U hU s).obj A ⟶ smoothGradedResolutionFunctor.obj ((toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj A)))

The comparison of the tensor-induced resolution with the total resolution of the tensor-induced coefficients: both are contracted onto Ind⊗_U^G A, and this is the morphism of degree zero over the identity of Ind⊗_U^G A given by the comparison theorem (TopRep.ResolutionContraction.gradedComparison), for the contraction of the tensor-induced resolution through the order on G ⧸ U.

theorem TauCeti.smoothTensorInducedGradedResolutionComparison_hom {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] {R : Type} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] [CompactSpace G] [Fintype (G ⧸ U)] [LinearOrder (G ⧸ U)] (A : SmoothDiscreteTopRep R ↥U) (hA : ∀ (a : ↑A.obj), a + a = 0) : (smoothTensorInducedGradedResolutionComparison U hU s A hA).hom = (smoothTensorInducedGradedResolutionContraction U hU s A hA).gradedComparison

The comparison is the comparison of the contraction of the tensor-induced resolution with the total resolution.

theorem TauCeti.isHomogeneous_smoothTensorInducedGradedResolutionComparison {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] {R : Type} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] [CompactSpace G] [Fintype (G ⧸ U)] [LinearOrder (G ⧸ U)] (A : SmoothDiscreteTopRep R ↥U) (hA : ∀ (a : ↑A.obj), a + a = 0) : LinearMap.IsHomogeneous (↑(TopRep.Hom.hom (smoothTensorInducedGradedResolutionComparison U hU s A hA).hom).toContinuousLinearMap) (smoothTensorInducedGradedResolutionPiece U hU s A) ((toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj A))).obj.gradedResolutionPiece 0

The comparison carries the total degree of the tensor-induced resolution to the degree of the total resolution.

theorem TauCeti.smoothTensorInducedGradedResolutionComparison_slotSum {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] {R : Type} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] [CompactSpace G] [Fintype (G ⧸ U)] [LinearOrder (G ⧸ U)] (A : SmoothDiscreteTopRep R ↥U) (hA : ∀ (a : ↑A.obj), a + a = 0) (y : PiTensorProduct R fun (x : G ⧸ U) => A.obj.gradedResolutionModule) : (TopRep.Hom.hom (smoothTensorInducedGradedResolutionComparison U hU s A hA).hom) ((PiTensorProduct.slotSum (G ⧸ U) fun (x : G ⧸ U) => A.obj.gradedResolutionDifferential) y) = ((toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj A))).obj.gradedResolutionDifferential ((TopRep.Hom.hom (smoothTensorInducedGradedResolutionComparison U hU s A hA).hom) y)

The comparison commutes with the differentials: it carries the slot sum of the total differential of A to the total differential of the tensor-induced coefficients.

@[simp]

theorem TauCeti.smoothTensorInducedGradedResolutionComparison_augmentation {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] {R : Type} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] [CompactSpace G] [Fintype (G ⧸ U)] [LinearOrder (G ⧸ U)] (A : SmoothDiscreteTopRep R ↥U) (hA : ∀ (a : ↑A.obj), a + a = 0) (x : ↑((toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj A))).obj) : (TopRep.Hom.hom (smoothTensorInducedGradedResolutionComparison U hU s A hA).hom) ((PiTensorProduct.map fun (x : G ⧸ U) => A.obj.gradedResolutionAugmentation) x) = ((toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj A))).obj.gradedResolutionAugmentation x

The comparison lies over the identity of the tensor-induced coefficients: it carries their augmentation into the tensor-induced resolution to their augmentation into the total resolution.

theorem TauCeti.smoothTensorInducedGradedResolutionComparison_tprod_const_mem_gradedResolutionPiece {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] {R : Type} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] [CompactSpace G] [Fintype (G ⧸ U)] [LinearOrder (G ⧸ U)] (A : SmoothDiscreteTopRep R ↥U) (hA : ∀ (a : ↑A.obj), a + a = 0) {n : ℕ} {z : A.obj.gradedResolutionModule} (hz : z ∈ A.obj.gradedResolutionPiece ↑n) : (TopRep.Hom.hom (smoothTensorInducedGradedResolutionComparison U hU s A hA).hom) ((PiTensorProduct.tprod R) fun (x : G ⧸ U) => z) ∈ ((toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj A))).obj.gradedResolutionPiece ↑(Fintype.card (G ⧸ U) * n)

The comparison carries the diagonal tensor z ⊗ ⋯ ⊗ z of a homogeneous element of degree n into degree l * n of the total resolution, for l the number of cosets.

theorem TauCeti.gradedResolutionTopRep_ρ_smoothTensorInducedGradedResolutionComparison_tprod_const {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] {R : Type} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] [CompactSpace G] [Fintype (G ⧸ U)] [LinearOrder (G ⧸ U)] (A : SmoothDiscreteTopRep R ↥U) (hA : ∀ (a : ↑A.obj), a + a = 0) {z : A.obj.gradedResolutionModule} (hinv : ∀ (u : ↥U), (A.obj.gradedResolutionTopRep.ρ u) z = z) (g : G) : (((toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj A))).obj.gradedResolutionTopRep.ρ g) ((TopRep.Hom.hom (smoothTensorInducedGradedResolutionComparison U hU s A hA).hom) ((PiTensorProduct.tprod R) fun (x : G ⧸ U) => z)) = (TopRep.Hom.hom (smoothTensorInducedGradedResolutionComparison U hU s A hA).hom) ((PiTensorProduct.tprod R) fun (x : G ⧸ U) => z)

The comparison carries the diagonal tensor z ⊗ ⋯ ⊗ z of a U-invariant element to a G-invariant element of the total resolution.

theorem TauCeti.gradedResolutionTopRepDifferential_smoothTensorInducedGradedResolutionComparison_eq_zero {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] {R : Type} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] [CompactSpace G] [Fintype (G ⧸ U)] [LinearOrder (G ⧸ U)] (A : SmoothDiscreteTopRep R ↥U) (hA : ∀ (a : ↑A.obj), a + a = 0) {z : A.obj.gradedResolutionModule} (hdz : A.obj.gradedResolutionDifferential z = 0) : (TopRep.Hom.hom ((toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj A))).obj.gradedResolutionTopRepDifferential) ((TopRep.Hom.hom (smoothTensorInducedGradedResolutionComparison U hU s A hA).hom) ((PiTensorProduct.tprod R) fun (x : G ⧸ U) => z)) = 0

The comparison carries the diagonal tensor z ⊗ ⋯ ⊗ z of a cocycle to a cocycle of the total resolution.

theorem TauCeti.gradedCohomologyClass_smoothTensorInducedGradedResolutionComparison {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] {R : Type} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] [CompactSpace G] [Fintype (G ⧸ U)] [LinearOrder (G ⧸ U)] (A : SmoothDiscreteTopRep R ↥U) (hA : ∀ (a : ↑A.obj), a + a = 0) {n : ℕ} {z : A.obj.gradedResolutionModule} (hz : z ∈ A.obj.gradedResolutionPiece ↑n) (hinv : ∀ (u : ↥U), (A.obj.gradedResolutionTopRep.ρ u) z = z) (hdz : A.obj.gradedResolutionDifferential z = 0) {y : ((toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj A))).obj.gradedResolutionModule} (hy : y ∈ ((toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj A))).obj.gradedResolutionPiece ↑(Fintype.card (G ⧸ U) * n)) (hyinv : ∀ (g : G), (((toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj A))).obj.gradedResolutionTopRep.ρ g) y = y) (hdy : (TopRep.Hom.hom ((toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj A))).obj.gradedResolutionTopRepDifferential) y = 0) (hyz : y = (TopRep.Hom.hom (smoothTensorInducedGradedResolutionComparison U hU s A hA).hom) ((PiTensorProduct.tprod R) fun (x : G ⧸ U) => z)) : (TopRep.gradedResolutionContraction ⋯).gradedCohomologyClass y hy hyinv hdy = smoothTensorInducedDiagonalClass U hU s A hA z hz hinv hdz

The norm of a cocycle on the total resolution. Let z be a U-invariant cocycle of degree n of the total resolution of A, and y the image under the comparison of its diagonal tensor z ⊗ ⋯ ⊗ z. Then y is a cocycle of degree l * n of the total resolution of Ind⊗_U^G A, fixed by G (smoothTensorInducedGradedResolutionComparison_tprod_const_mem_gradedResolutionPiece, gradedResolutionTopRep_ρ_smoothTensorInducedGradedResolutionComparison_tprod_const, gradedResolutionTopRepDifferential_smoothTensorInducedGradedResolutionComparison_eq_zero), and its class, for any such proofs hy, hyinv and hdy, is the norm of z.