Smooth tensor induction of trivial F₂ coefficients

Smooth tensor induction (TauCeti.smoothTensorInductionFunctor) of the canonical trivial 𝔽₂ coefficient object is again the canonical trivial coefficient object of the ambient group.

The isomorphism multiplies the tensor factors. It is the coefficient identification needed before the cochain-level Evens norm can be read as a class in TauCeti.cohomF2 G rather than in the cohomology of an abstract tensor-induced coefficient object.

Main definitions

• TauCeti.smoothTensorInducedTrivialF2Iso: tensor induction of trivial 𝔽₂ coefficients is the canonical trivial 𝔽₂ coefficient object.

References

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

@[instance_reducible]

noncomputable def TauCeti.quotientFintype (G : Type v) [Group G] (U : Subgroup G) [U.FiniteIndex] : Fintype (G ⧸ U)

The finite quotient indexing the tensor factors of tensor induction.

noncomputable def TauCeti.smoothTensorInducedTrivialF2Tprod (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] (x : G ⧸ U → (DiscreteRep.trivialF2 ↥U).V) : (DiscreteRep.tensorInduced U hU s (DiscreteRep.trivialF2 ↥U)).V

The pure tensor in the smooth tensor induction of trivial 𝔽₂ coefficients.

Its characteristic equation smoothTensorInducedTrivialF2Tprod_eq lets morphisms use their PiTensorProduct.tprod computation rules without exposing this definition.

theorem TauCeti.smoothTensorInducedTrivialF2Tprod_eq (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] (x : G ⧸ U → (DiscreteRep.trivialF2 ↥U).V) : smoothTensorInducedTrivialF2Tprod G U hU s x = (PiTensorProduct.tprod ℤ) x

The named tensor is the underlying pure tensor, transported to the carrier of tensor induction.

noncomputable def TauCeti.smoothTensorInducedTrivialF2Iso (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] : (smoothTensorInductionFunctor ℤ G U hU s).obj { obj := trivialF2 ↥U, property := ⋯ } ≅ { obj := trivialF2 G, property := ⋯ }

Smooth tensor induction of the canonical trivial 𝔽₂ coefficient object is isomorphic to the canonical trivial 𝔽₂ coefficient object of the ambient group.

On carriers the forward map multiplies the tensor factors.

theorem TauCeti.smoothTensorInducedTrivialF2Iso_hom_apply_tprod (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] (x : G ⧸ U → (DiscreteRep.trivialF2 ↥U).V) : (trivialF2Equiv G) ((TopRep.Hom.hom (smoothTensorInducedTrivialF2Iso G U hU s).hom.hom) (smoothTensorInducedTrivialF2Tprod G U hU s x)) = ∏ i : G ⧸ U, (trivialF2Equiv ↥U) (x i)

On a pure tensor, the smooth trivial-𝔽₂ tensor-induction isomorphism multiplies the underlying ZMod 2 values.

theorem TauCeti.smoothTensorInducedTrivialF2Iso_hom_apply_piTensorProduct_tprod (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] (x : G ⧸ U → (DiscreteRep.trivialF2 ↥U).V) : (trivialF2Equiv G) ((TopRep.Hom.hom (smoothTensorInducedTrivialF2Iso G U hU s).hom.hom) ((PiTensorProduct.tprod ℤ) x)) = ∏ i : G ⧸ U, (trivialF2Equiv ↥U) (x i)

smoothTensorInducedTrivialF2Iso_hom_apply_tprod, stated for the raw pure tensor PiTensorProduct.tprod ℤ x formed with the ℤ-module structure of the DiscreteRep. Rewriting cannot fold such a tensor back into smoothTensorInducedTrivialF2Tprod across that instance, so the computation rule is transported along smoothTensorInducedTrivialF2Tprod_eq here once.