Documentation

TauCeti.RepresentationTheory.Homological.ContCohomology.Coinduced.Quotient

The cokernel of the unit of coinduction #

For a subgroup U of a topological group G and a discrete G-module M, the unit of coinduction TauCeti.DiscreteCoind.unit G U M embeds M into Coind_U^G M by its orbit maps,

M ↪ Coind_U^G M,   m ↦ (x ↦ x • m).

This file builds its cokernel Coind_U^G M ⧸ M as a discrete G-module and the resulting short exact sequence 0 → M → Coind_U^G M → Coind_U^G M ⧸ M → 0 of discrete G-modules. For U = ⊥ it is the sequence on which dimension shifting runs (TauCeti/RepresentationTheory/Homological/ContCohomology/DimensionShifting/Basic.lean); for an open subgroup U it feeds the reduction of finiteness of cohomology to an open subgroup.

Main definitions #

Main results #

Implementation notes #

As for TauCeti.DiscreteCoind, the quotient is a type synonym carrying the discrete topology; the quotient topology inherited from QuotientAddGroup is not the one used for coefficients. Its G-action is induced by the right-translation action on Coind_U^G M, which preserves the image of M because the embedding is G-equivariant, and it is continuous because the stabilizer of a class contains the open stabilizer of any representative.

Compactness of G makes the right-translation action on Coind_U^G M continuous. The underlying quotient and its algebraic action do not require compactness, but its ContinuousSMul instance does.

source
def TauCeti.ContCohomology.CoindQuotient (G : Type u) [Group G] [TopologicalSpace G] (U : Subgroup G) (M : Type v) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] :
Type (max (max u v) v u)

The cokernel Coind_U^G M ⧸ M of the unit of coinduction, the quotient of Coind_U^G M by the image of the embedding TauCeti.DiscreteCoind.unit G U M, carrying the discrete topology. For U = ⊥ this is the dimension-shifting module Coind_1^G M ⧸ M.

Equations
Instances For
    source
    @[instance_reducible]
    instance TauCeti.ContCohomology.CoindQuotient.instAddCommGroup (G : Type u) [Group G] [TopologicalSpace G] (U : Subgroup G) (M : Type v) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] :
    AddCommGroup (CoindQuotient G U M)

    Coind_U^G M ⧸ M is an additive group, as a quotient of Coind_U^G M.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[instance_reducible]
    instance TauCeti.ContCohomology.CoindQuotient.instTopologicalSpace (G : Type u) [Group G] [TopologicalSpace G] (U : Subgroup G) (M : Type v) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] :
    TopologicalSpace (CoindQuotient G U M)

    Coind_U^G M ⧸ M carries the discrete topology.

    Equations
    source
    instance TauCeti.ContCohomology.CoindQuotient.instDiscreteTopology (G : Type u) [Group G] [TopologicalSpace G] (U : Subgroup G) (M : Type v) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] :
    DiscreteTopology (CoindQuotient G U M)

    The topology on Coind_U^G M ⧸ M is discrete.

    source
    def TauCeti.ContCohomology.CoindQuotient.mk (G : Type u) [Group G] [TopologicalSpace G] (U : Subgroup G) (M : Type v) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] :
    DiscreteCoind G U M →+ CoindQuotient G U M

    The projection Coind_U^G M → Coind_U^G M ⧸ M.

    Equations
    Instances For
      source
      theorem TauCeti.ContCohomology.CoindQuotient.mk_surjective {G : Type u} [Group G] [TopologicalSpace G] {U : Subgroup G} {M : Type v} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] :
      Function.Surjective ⇑(mk G U M)

      The projection Coind_U^G M → Coind_U^G M ⧸ M is surjective.

      source
      @[simp]
      theorem TauCeti.ContCohomology.CoindQuotient.mk_eq_zero_iff {G : Type u} [Group G] [TopologicalSpace G] {U : Subgroup G} {M : Type v} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] {f : DiscreteCoind G U M} :
      (mk G U M) f = 0 ↔ f ∈ (DiscreteCoind.unit G U M).toAddMonoidHom.range

      A coinduced element dies in the quotient exactly when it is in the image of the unit.

      source
      theorem TauCeti.ContCohomology.CoindQuotient.induction_on {G : Type u} [Group G] [TopologicalSpace G] {U : Subgroup G} {M : Type v} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] {motive : CoindQuotient G U M → Prop} (q : CoindQuotient G U M) (h : ∀ (f : DiscreteCoind G U M), motive ((mk G U M) f)) :
      motive q

      Induction on Coind_U^G M ⧸ M: a property of the classes of all coinduced elements holds for every element of the quotient.

      source
      instance TauCeti.ContCohomology.CoindQuotient.instFiniteOfDiscreteCoind {G : Type u} [Group G] [TopologicalSpace G] {U : Subgroup G} {M : Type v} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] [Finite (DiscreteCoind G U M)] :
      Finite (CoindQuotient G U M)

      Coind_U^G M ⧸ M is finite when Coind_U^G M is.

      source
      @[instance_reducible]
      instance TauCeti.ContCohomology.CoindQuotient.instDistribMulAction {G : Type u} [Group G] [TopologicalSpace G] {U : Subgroup G} {M : Type v} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] :
      DistribMulAction G (CoindQuotient G U M)

      Right translation on Coind_U^G M, descended to the quotient; the image of M is preserved because the embedding is equivariant.

      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[simp]
      theorem TauCeti.ContCohomology.CoindQuotient.mk_smul {G : Type u} [Group G] [TopologicalSpace G] {U : Subgroup G} {M : Type v} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] (g : G) (f : DiscreteCoind G U M) :
      (mk G U M) (g • f) = g • (mk G U M) f

      The projection is G-equivariant.

      source
      theorem TauCeti.ContCohomology.CoindQuotient.smul_eq_self_of_forall_smul_eq_self {G : Type u} [Group G] [TopologicalSpace G] {U : Subgroup G} {M : Type v} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] [U.Normal] (htriv : ∀ (u : ↥U) (m : M), u • m = m) {g : G} (hg : g ∈ U) (q : CoindQuotient G U M) :
      g • q = q

      A normal subgroup acting trivially on M acts trivially on Coind_U^G M ⧸ M, as it does on Coind_U^G M (TauCeti.DiscreteCoind.smul_eq_self_of_forall_smul_eq_self).

      source
      def TauCeti.ContCohomology.coindShortExact (G : Type u) [Group G] [TopologicalSpace G] (U : Subgroup G) (M : Type v) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] :
      DiscreteShortExact G M (DiscreteCoind G U M) (CoindQuotient G U M)

      The short exact sequence 0 → M → Coind_U^G M → Coind_U^G M ⧸ M → 0 of discrete G-modules given by the unit of coinduction. For U = ⊥ it is the sequence on which dimension shifting runs.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.ContCohomology.coindShortExact_incl (G : Type u) [Group G] [TopologicalSpace G] (U : Subgroup G) (M : Type v) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] :
        (coindShortExact G U M).incl = (DiscreteCoind.unit G U M).toAddMonoidHom

        The first map of the short exact sequence of the unit is the unit M → Coind_U^G M.

        source
        @[simp]
        theorem TauCeti.ContCohomology.coindShortExact_proj (G : Type u) [Group G] [TopologicalSpace G] (U : Subgroup G) (M : Type v) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] :
        (coindShortExact G U M).proj = CoindQuotient.mk G U M

        The second map of the short exact sequence of the unit is the projection Coind_U^G M → Coind_U^G M ⧸ M.

        source
        theorem TauCeti.ContCohomology.precomp_coindShortExact_inclDistribMulActionHom_surjective (G : Type u) [Group G] [TopologicalSpace G] (U : Subgroup G) (M : Type v) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] {N : Type u_1} [AddCommGroup N] [DistribMulAction G N] :
        Function.Surjective ⇑(InternalHom.precomp G (coindShortExact G U M).inclDistribMulActionHom)

        Homomorphisms out of M extend along the unit of coinduction: precomposition with the inclusion of coindShortExact is surjective on internal homs into any N, since φ : M →+ N extends to Coind_U^G M as f ↦ φ (f 1). So the dual sequence of coindShortExact (TauCeti.ContCohomology.DiscreteShortExact.dual) exists for all coefficients.

        source
        instance TauCeti.ContCohomology.CoindQuotient.instContinuousSMul {G : Type u} [Group G] [TopologicalSpace G] {U : Subgroup G} {M : Type v} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [IsTopologicalGroup G] [CompactSpace G] :
        ContinuousSMul G (CoindQuotient G U M)

        The action on the quotient is continuous: the stabilizer of a class contains the stabilizer of any representative, which is open.