← all areas

Namespace GroupCohomology 10 theorems

RepCokernel 1 · RepImage 1 · RepPi 8

GroupCohomology.RepCokernel 1

• Cokernel sequence of an injective morphism of representations is short exact GroupCohomology.RepCokernel.seq_shortExact 0 below · cited by 2 · depth 27

GroupCohomology.RepImage 1

• Image, target and cokernel form a short exact sequence GroupCohomology.RepImage.seq_shortExact 0 below · cited by 2 · depth 19

GroupCohomology.RepPi 8

• Assembling local conditions across a product of coinduced representations GroupCohomology.RepPi.forall_exists_comp_proj_and_iff_exists_eq_comp_of_coind 0 below · cited by 2 · depth 19
• H¹(G,Hom(R,prod Xᵢ)) is the product of H¹(G,Hom(R,Xᵢ)) GroupCohomology.RepPi.map_ihom_proj_one_injective_and_surjective 0 below · cited by 1 · depth 19
• Order of Tate ̂ H⁰ of a product representation GroupCohomology.RepPi.natCard_tateH0_obj_eq_prod_of_subsingleton 1 below · cited by 2 · depth 21
• Factorwise vanishing of ̂ H⁻¹ passes to products GroupCohomology.RepPi.subsingleton_tateHneg1_obj 1 below · cited by 2 · depth 21
• Tate ̂ H⁰ of a product of representations GroupCohomology.RepPi.nonempty_tateH0_obj_linearEquiv 0 below · cited by 1 · depth 22
• ̂ H⁻¹ of a product of representations splits GroupCohomology.RepPi.nonempty_tateHneg1_obj_linearEquiv 0 below · cited by 1 · depth 22
• Vanishing of Hⁿ for a product of representations GroupCohomology.RepPi.isZero_groupCohomology_obj 0 below · cited by 1 · depth 23
• Cohomology commutes with products of representations GroupCohomology.RepPi.bijective_pi_map_proj 0 below · cited by 1 · depth 24