Kernels and cokernels in TopRep k G

For a morphism f : A ⟶ B of continuous representations, the kernel of the underlying linear map is an invariant submodule of A and the range is an invariant submodule of B. With the subspace and quotient topologies they carry continuous representations (ContRepresentation.subrepresentation, ContRepresentation.quotient), and they are the kernel and the cokernel of f in TopRep k G, as for TopModuleCat.ker and TopModuleCat.coker in the category of topological modules.

Main definitions

• TopRep.ker, TopRep.kerι: the kernel of a morphism, with its inclusion.
• TopRep.coker, TopRep.cokerπ: the cokernel of a morphism, with its projection.

Main results

• TopRep.isLimitKer: TopRep.kerι f is a kernel of f.
• TopRep.isColimitCoker: TopRep.cokerπ f is a cokernel of f.
• TopRep.exact_kerι, TopRep.exact_cokerπ: the underlying maps of kerι f, f and of f, cokerπ f are exact.

@[reducible, inline]

abbrev TopRep.ker {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Monoid G] {A B : TopRep k G} (f : A ⟶ B) : TopRep k G

The kernel of a morphism of continuous representations: the kernel of the underlying linear map with the subspace topology and the restricted action.

def TopRep.kerι {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Monoid G] {A B : TopRep k G} (f : A ⟶ B) : ker f ⟶ A

The inclusion of the kernel of a morphism.

@[simp]

theorem TopRep.kerι_apply {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Monoid G] {A B : TopRep k G} (f : A ⟶ B) (a : ↑(ker f)) : (Hom.hom (kerι f)) a = ↑a

The inclusion of the kernel sends a vector to the same vector of A.

theorem TopRep.kerι_injective {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Monoid G] {A B : TopRep k G} (f : A ⟶ B) : Function.Injective ⇑(Hom.hom (kerι f))

The inclusion of the kernel is injective.

theorem TopRep.exact_kerι {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Monoid G] {A B : TopRep k G} (f : A ⟶ B) : Function.Exact ⇑(Hom.hom (kerι f)) ⇑(Hom.hom f)

The inclusion of the kernel of f is exact at A with f.

@[simp]

theorem TopRep.kerι_comp {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Monoid G] {A B : TopRep k G} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (kerι f) f = 0

The inclusion of the kernel of f composed with f is zero.

@[simp]

theorem TopRep.kerι_comp_assoc {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Monoid G] {A B : TopRep k G} (f : A ⟶ B) {Z : TopRep k G} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (kerι f) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp 0 h

The inclusion of the kernel of f composed with f is zero.

def TopRep.isLimitKer {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Monoid G] {A B : TopRep k G} (f : A ⟶ B) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (kerι f) ⋯)

TopRep.kerι f is a kernel of f in TopRep k G.

@[reducible, inline]

abbrev TopRep.coker {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Monoid G] {A B : TopRep k G} (f : A ⟶ B) : TopRep k G

The cokernel of a morphism of continuous representations: the quotient by the range of the underlying linear map, with the quotient topology and the descended action.

def TopRep.cokerπ {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Monoid G] {A B : TopRep k G} (f : A ⟶ B) : B ⟶ coker f

The projection onto the cokernel of a morphism.

@[simp]

theorem TopRep.cokerπ_apply {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Monoid G] {A B : TopRep k G} (f : A ⟶ B) (b : ↑B) : (Hom.hom (cokerπ f)) b = Submodule.Quotient.mk b

The projection onto the cokernel sends a vector to its class.

theorem TopRep.cokerπ_surjective {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Monoid G] {A B : TopRep k G} (f : A ⟶ B) : Function.Surjective ⇑(Hom.hom (cokerπ f))

The projection onto the cokernel is surjective.

theorem TopRep.exact_cokerπ {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Monoid G] {A B : TopRep k G} (f : A ⟶ B) : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom (cokerπ f))

f is exact at B with the projection onto its cokernel.

@[simp]

theorem TopRep.comp_cokerπ {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Monoid G] {A B : TopRep k G} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp f (cokerπ f) = 0

f composed with the projection onto its cokernel is zero.

@[simp]

theorem TopRep.comp_cokerπ_assoc {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Monoid G] {A B : TopRep k G} (f : A ⟶ B) {Z : TopRep k G} (h : coker f ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (cokerπ f) h) = CategoryTheory.CategoryStruct.comp 0 h

f composed with the projection onto its cokernel is zero.

def TopRep.isColimitCoker {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Monoid G] {A B : TopRep k G} (f : A ⟶ B) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (cokerπ f) ⋯)

TopRep.cokerπ f is a cokernel of f in TopRep k G.

@[simp]

theorem TopRep.natCast_smul_id_apply {k : Type u_3} {G : Type u_4} [CommRing k] [TopologicalSpace k] [Monoid G] (A : TopRep k G) (ℓ : ℕ) (a : ↑A) : (Hom.hom (↑ℓ • CategoryTheory.CategoryStruct.id A)) a = ℓ • a

Multiplication by the natural number ℓ on a continuous representation acts on the carrier as a ↦ ℓ • a.

theorem TopRep.card_ker_natCast_smul_id_lt {k : Type u_3} {G : Type u_4} [CommRing k] [TopologicalSpace k] [Monoid G] (A : TopRep k G) (ℓ : ℕ) [Finite ↑A] (x : ↑A) (hx : ℓ • x ≠ 0) : Nat.card ↑(ker (↑ℓ • CategoryTheory.CategoryStruct.id A)) < Nat.card ↑A

The ℓ-torsion of a finite representation is strictly smaller than the representation when ℓ does not kill it.

theorem TopRep.card_coker_kerι_natCast_smul_id_lt {k : Type u_3} {G : Type u_4} [CommRing k] [TopologicalSpace k] [Monoid G] (A : TopRep k G) (ℓ : ℕ) [Finite ↑A] (y : ↑A) (hy0 : y ≠ 0) (hy : ℓ • y = 0) : Nat.card ↑(coker (kerι (↑ℓ • CategoryTheory.CategoryStruct.id A))) < Nat.card ↑A

The quotient of a finite representation by its ℓ-torsion is strictly smaller than the representation when a nonzero vector is killed by ℓ.