Coinduction as a functor of smooth discrete representations

For a compact topological group G and a subgroup U, this file packages the discrete coinduced module TauCeti.DiscreteCoind in the categorical language of smooth discrete representations, and compares it with Mathlib's algebraic coinduction Representation.coind. The unbundled module TauCeti.coind is transported to the categorical language through the smooth-discrete dictionary (TauCeti.toSmoothDiscrete, TauCeti.ofSmoothDiscrete).

Main definitions

• TauCeti.coindDiscreteFunctor: coinduction from discrete U-representations to discrete G-representations, with objects TauCeti.coindDiscreteRep;
• TauCeti.coindFunctor: coinduction from smooth discrete U-representations to smooth discrete G-representations, with objects TauCeti.coindTopRep;
• TauCeti.coindCounit and TauCeti.coindCounitNatTrans: evaluation at 1 as the counit of coinduction, objectwise and natural in the coefficient representation;
• TauCeti.coindTraceHom: for finite-index U, the trace as a morphism of smooth discrete G-representations;
• TauCeti.discreteCoindEquivAlgebraic: for an open subgroup U, the linear equivalence between locally constant coinduction and Mathlib's Representation.coindV;
• TauCeti.algebraicCoindCounit: evaluation at 1 on algebraic coinduction with its discrete topology, for comparing the two restriction–evaluation Shapiro maps.

Main results

• TauCeti.isLocallyConstant_representationCoindV: for an open subgroup, every algebraically coinduced function is automatically locally constant;
• TauCeti.topologicalCoindIsoAlgebraic: for an open subgroup, TauCeti.coindTopRep is isomorphic to Mathlib's Representation.coind regarded as a smooth discrete representation (TauCeti.algebraicCoindAsSmooth), by the identity on underlying functions.

theorem TauCeti.instContinuousSMulOfSmoothDiscreteCoind {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (A : SmoothDiscreteTopRep R G) : ContinuousSMul G ↑A.obj

@[reducible, inline]

noncomputable abbrev TauCeti.coindDiscreteRep (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : Subgroup G) (A : DiscreteRep R ↥U) : DiscreteRep R G

The locally constant coinduced module, bundled as a discrete representation of G.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.coindDiscreteFunctor (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : Subgroup G) : CategoryTheory.Functor (DiscreteRep R ↥U) (DiscreteRep R G)

Coinduction from discrete U-representations to discrete G-representations.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.coindDiscreteFunctor_obj (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : Subgroup G) (A : DiscreteRep R ↥U) : (coindDiscreteFunctor R G U).obj A = coindDiscreteRep R G U A

The object part of discrete coinduction is the locally constant coinduced representation.

@[simp]

theorem TauCeti.coindDiscreteFunctor_map_apply (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : Subgroup G) {A B : DiscreteRep R ↥U} (f : A ⟶ B) (a : DiscreteCoind G U A.V) (g : G) : ((CategoryTheory.eqToHom ⋯) (((coindDiscreteFunctor R G U).map f) ((CategoryTheory.eqToHom ⋯) a))) g = f.toLinearMap (a g)

Discrete coinduction maps act pointwise on their locally constant functions. The explicit object transports identify the opaque functor's objects with coindDiscreteRep.

@[reducible, inline]

noncomputable abbrev TauCeti.coindTopRep (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : Subgroup G) (A : SmoothDiscreteTopRep R ↥U) : SmoothDiscreteTopRep R G

The locally constant coinduced module, bundled as a smooth discrete representation of G.

Equations

• TauCeti.coindTopRep R G U A = (TauCeti.toSmoothDiscrete R G).obj (TauCeti.coindDiscreteRep R G U ((TauCeti.ofSmoothDiscrete R ↥U).obj A))

noncomputable def TauCeti.coindCounit (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : Subgroup G) (A : SmoothDiscreteTopRep R ↥U) : ContIntertwiningMap (TopRep.res U.subtype (coindTopRep R G U A).obj).ρ A.obj.ρ

Evaluation at 1 as the coinduction counit, from the restriction of the coinduced representation to its coefficient representation.

Equations

• TauCeti.coindCounit R G U A = { toLinearMap := TauCeti.DiscreteCoind.evalLinear G U (↑A.obj) R, cont := ⋯, isIntertwining' := ⋯ }

@[simp]

theorem TauCeti.coindCounit_apply (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : Subgroup G) (A : SmoothDiscreteTopRep R ↥U) (f : DiscreteCoind G U ↑A.obj) : (coindCounit R G U A) f = f 1

The counit of coinduction evaluates a coinduced function at the identity.

noncomputable def TauCeti.coindTraceHom (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : Subgroup G) [U.FiniteIndex] (A : SmoothDiscreteTopRep R G) : (coindTopRep R G U { obj := TopRep.res U.subtype A.obj, property := ⋯ }).obj ⟶ A.obj

The trace packaged as a morphism of smooth discrete G-representations for a finite-index subgroup U.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.coindTraceHom_apply (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : Subgroup G) [U.FiniteIndex] (A : SmoothDiscreteTopRep R G) (f : DiscreteCoind G U ↑A.obj) : (CategoryTheory.ConcreteCategory.hom (coindTraceHom R G U A)) f = (DiscreteCoind.trace G U ↑A.obj) f

noncomputable def TauCeti.coindFunctor (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : Subgroup G) : CategoryTheory.Functor (SmoothDiscreteTopRep R ↥U) (SmoothDiscreteTopRep R G)

Coinduction from smooth discrete U-representations to smooth discrete G-representations.

Equations

• TauCeti.coindFunctor R G U = (TauCeti.ofSmoothDiscrete R ↥U).comp ((TauCeti.coindDiscreteFunctor R G U).comp (TauCeti.toSmoothDiscrete R G))

@[simp]

theorem TauCeti.coindFunctor_obj (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : Subgroup G) (A : SmoothDiscreteTopRep R ↥U) : (coindFunctor R G U).obj A = coindTopRep R G U A

The object part of smooth discrete coinduction is the bundled locally constant coinduced representation.

@[simp]

theorem TauCeti.coindFunctor_map_apply (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : Subgroup G) {A B : SmoothDiscreteTopRep R ↥U} (f : A ⟶ B) (a : DiscreteCoind G U ↑A.obj) (g : G) : (have this := (((TopRep.Hom.hom (CategoryTheory.eqToHom ⋯)).comp (TopRep.Hom.hom ((coindFunctor R G U).map f).hom)).comp (TopRep.Hom.hom (CategoryTheory.eqToHom ⋯))) a; this) g = (TopRep.Hom.hom f.hom) (a g)

Smooth discrete coinduction maps act pointwise on their locally constant functions. The object transports identify the opaque composite functor's objects with coindTopRep.

noncomputable def TauCeti.coindCounitNatTrans (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : Subgroup G) : (coindFunctor R G U).comp (smoothDiscreteResFunctor R G U) ⟶ CategoryTheory.Functor.id (SmoothDiscreteTopRep R ↥U)

Evaluation at 1, natural in the smooth discrete coefficient representation.

Equations

• TauCeti.coindCounitNatTrans R G U = { app := TauCeti.coindCounitApp✝ R G U, naturality := ⋯ }

@[simp]

theorem TauCeti.coindCounitNatTrans_app_apply (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : Subgroup G) (A : SmoothDiscreteTopRep R ↥U) (f : DiscreteCoind G U ↑A.obj) : (have this := (TopRep.Hom.hom ((coindCounitNatTrans R G U).app A).hom).comp (TopRep.Hom.hom (CategoryTheory.eqToHom ⋯)); this) f = f 1

The components of the coinduction counit evaluate at 1. The object transport identifies the restricted opaque coinduced object with the restriction of coindTopRep.

theorem TauCeti.isLocallyConstant_representationCoindV (R : Type u) [Semiring R] (G : Type v) [Group G] [TopologicalSpace G] [ContinuousMul G] (U : OpenSubgroup G) {A : Type w} [AddCommMonoid A] [Module R A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction (↥↑U) A] [SMulCommClass (↥↑U) R A] [ContinuousSMul (↥↑U) A] (f : ↥(Representation.coindV (↑U).subtype (Representation.ofDistribMulAction R (↥↑U) A))) : IsLocallyConstant ↑f

An algebraically coinduced function from an open subgroup is locally constant when the coefficient action is continuous and the coefficient space is discrete.

theorem TauCeti.instContinuousSMulSubtypeMemSubgroupVObjTopRepIsSmoothDiscrete (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (A : SmoothDiscreteTopRep R ↥↑U) : ContinuousSMul ↥↑U ↑A.obj

theorem TauCeti.instSMulCommClassSubtypeMemSubgroupVObjTopRepIsSmoothDiscrete (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] (U : OpenSubgroup G) (A : SmoothDiscreteTopRep R ↥↑U) : SMulCommClass (↥↑U) R ↑A.obj

theorem TauCeti.instSMulCommClassDiscreteCoindVSubtypeMemSubgroupObjTopRepIsSmoothDiscrete (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (A : SmoothDiscreteTopRep R ↥↑U) : SMulCommClass G R (DiscreteCoind G ↑U ↑A.obj)

noncomputable def TauCeti.discreteCoindEquivAlgebraic (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (A : SmoothDiscreteTopRep R ↥↑U) : DiscreteCoind G ↑U ↑A.obj ≃ₗ[R] ↥(Representation.coindV (↑U).subtype (Representation.ofDistribMulAction R ↥↑U ↑A.obj))

For an open subgroup, locally constant coinduction is linearly equivalent to Mathlib's algebraic Representation.coindV, which carries the action Representation.coind. Both directions preserve the underlying function on G.

Openness is used only in the inverse direction: it makes every algebraically coinduced function locally constant.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.discreteCoindEquivAlgebraic_apply (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (A : SmoothDiscreteTopRep R ↥↑U) (f : DiscreteCoind G ↑U ↑A.obj) (g : G) : ↑((discreteCoindEquivAlgebraic R G U A) f) g = f g

The comparison sends a locally constant coinduced function to the same underlying algebraically coinduced function.

@[simp]

theorem TauCeti.discreteCoindEquivAlgebraic_symm_apply (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (A : SmoothDiscreteTopRep R ↥↑U) (f : ↥(Representation.coindV (↑U).subtype (Representation.ofDistribMulAction R ↥↑U ↑A.obj))) (g : G) : ((discreteCoindEquivAlgebraic R G U A).symm f) g = ↑f g

The inverse comparison sends an algebraically coinduced function to the same underlying function, now equipped with its automatic local constancy.

@[simp]

theorem TauCeti.discreteCoindEquivAlgebraic_smul (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (A : SmoothDiscreteTopRep R ↥↑U) (g : G) (f : DiscreteCoind G ↑U ↑A.obj) : (discreteCoindEquivAlgebraic R G U A) (g • f) = ((Representation.coind (↑U).subtype (Representation.ofDistribMulAction R ↥↑U ↑A.obj)) g) ((discreteCoindEquivAlgebraic R G U A) f)

The locally constant/algebraic coinduction comparison intertwines the right-translation actions of G.

@[reducible, inline]

noncomputable abbrev TauCeti.algebraicCoindDiscreteRep (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (A : SmoothDiscreteTopRep R ↥↑U) [CompactSpace G] : DiscreteRep R G

Mathlib's algebraic coinduction, equipped with the discrete topology and the continuous actions transported from locally constant coinduction.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.algebraicCoindDiscreteRep_ρ (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (A : SmoothDiscreteTopRep R ↥↑U) [CompactSpace G] : (algebraicCoindDiscreteRep R G U A).ρ = Representation.coind (↑U).subtype (Representation.ofDistribMulAction R ↥↑U ↑A.obj)

The representation carried by algebraicCoindDiscreteRep is Mathlib's Representation.coind, not merely an abstractly isomorphic action.

@[reducible, inline]

noncomputable abbrev TauCeti.algebraicCoindAsSmooth (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (A : SmoothDiscreteTopRep R ↥↑U) [CompactSpace G] : SmoothDiscreteTopRep R G

Algebraic coinduction from an open subgroup, regarded as a smooth discrete topological representation.

Equations

• TauCeti.algebraicCoindAsSmooth R G U A = (TauCeti.toSmoothDiscrete R G).obj (TauCeti.algebraicCoindDiscreteRep R G U A)

noncomputable def TauCeti.algebraicCoindCounit (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (A : SmoothDiscreteTopRep R ↥↑U) [CompactSpace G] : ContIntertwiningMap (TopRep.res (↑U).subtype (algebraicCoindAsSmooth R G U A).obj).ρ A.obj.ρ

Evaluation at 1 on algebraic coinduction, with the discrete topology. Over a commutative ring this is the counit of Mathlib's restriction–coinduction adjunction.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.algebraicCoindCounit_apply (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (A : SmoothDiscreteTopRep R ↥↑U) [CompactSpace G] (f : ↥(Representation.coindV (↑U).subtype (Representation.ofDistribMulAction R ↥↑U ↑A.obj))) : (algebraicCoindCounit R G U A) f = ↑f 1

The algebraic counit evaluates the underlying equivariant function at 1.

noncomputable def TauCeti.topologicalCoindIsoAlgebraic (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (A : SmoothDiscreteTopRep R ↥↑U) [CompactSpace G] : coindTopRep R G (↑U) A ≅ algebraicCoindAsSmooth R G U A

Locally constant topological coinduction from an open subgroup agrees with Mathlib's algebraic coinduction. The isomorphism is the identity on the underlying equivariant functions.

Equations

• TauCeti.topologicalCoindIsoAlgebraic R G U A = (TauCeti.toSmoothDiscrete R G).mapIso (TauCeti.discreteCoindIsoAlgebraic✝ R G U A)

@[simp]

theorem TauCeti.topologicalCoindIsoAlgebraic_hom_hom_hom_apply_coe (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (A : SmoothDiscreteTopRep R ↥↑U) [CompactSpace G] (f : DiscreteCoind G ↑U ↑A.obj) (g : G) : ↑((TopRep.Hom.hom (topologicalCoindIsoAlgebraic R G U A).hom.hom) f) g = f g

The forward map of the topological/algebraic comparison leaves every value unchanged.

@[simp]

theorem TauCeti.topologicalCoindIsoAlgebraic_inv_hom_hom_apply_coe (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (A : SmoothDiscreteTopRep R ↥↑U) [CompactSpace G] (f : ↥(Representation.coindV (↑U).subtype (Representation.ofDistribMulAction R ↥↑U ↑A.obj))) (g : G) : (have this := (TopRep.Hom.hom (topologicalCoindIsoAlgebraic R G U A).inv.hom) f; this) g = ↑f g

The inverse map of the topological/algebraic comparison leaves every value unchanged.

theorem TauCeti.topologicalCoindIsoAlgebraic_hom_comp_counit {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) [CompactSpace G] (B : SmoothDiscreteTopRep R ↥↑U) : CategoryTheory.CategoryStruct.comp ((TopRep.resFunctor (↑U).subtype).map (topologicalCoindIsoAlgebraic R G U B).hom.hom) (TopRep.ofHom (algebraicCoindCounit R G U B)) = TopRep.ofHom (coindCounit R G (↑U) B)

The topological/algebraic coinduction comparison preserves the evaluation counit.

theorem TauCeti.topologicalCoindIsoAlgebraic_hom_comp_counit_assoc {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) [CompactSpace G] (B : SmoothDiscreteTopRep R ↥↑U) {Z : TopRep R ↥↑U} (h : TopRep.of B.obj.ρ ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopRep.ofHom (ContIntertwiningMap.restrict (↑U).subtype (TopRep.Hom.hom (topologicalCoindIsoAlgebraic R G U B).hom.hom))) (CategoryTheory.CategoryStruct.comp (TopRep.ofHom (algebraicCoindCounit R G U B)) h) = CategoryTheory.CategoryStruct.comp (TopRep.ofHom (coindCounit R G (↑U) B)) h

The topological/algebraic coinduction comparison preserves the evaluation counit.

theorem TauCeti.algebraicCoindCounit_toLinearMap {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : OpenSubgroup G) (A : SmoothDiscreteTopRep R ↥↑U) : ↑(algebraicCoindCounit R G U A).toContinuousLinearMap = (Rep.Hom.hom ((Rep.resCoindAdjunction R (↑U).subtype).counit.app (Rep.of (Representation.ofDistribMulAction R ↥↑U ↑A.obj)))).toLinearMap

The continuous algebraic evaluation counit is the counit of Mathlib's algebraic restriction–coinduction adjunction after forgetting continuity.