← all areas

Namespace Rep 188 theorems

— 170 · IsTateCupProduct 18

directly in Rep 170

• Dimension-shifting short exact sequence into a coinduced representation Rep.exists_shortExact_coind_res 2 below · cited by 3 · depth 14
• Smoothness of the cyclotomic dual twist of a mod p Galois module Rep.dualTwist_cycloChar_smooth 1 below · cited by 6 · depth 15
• Cyclotomic dual twist stays unramified outside Sni p Rep.dualTwist_cycloChar_unramifiedOutside 2 below · cited by 3 · depth 15
• Vanishing of invariants of a twisted k-linear dual Rep.dualTwist_of_invariants_eq_bot_of_forall_linearMap_eq_zero 0 below · cited by 1 · depth 15
• Dévissage of a non-simple smooth finite representation Rep.exists_devissage_of_not_simple 0 below · cited by 2 · depth 15
• Coinduction preserves level-smoothness along a finite-index subgroup Rep.exists_level_coind_apply_eq_self 0 below · cited by 6 · depth 15
• Finite-dimensionality and dimension of a coinduced representation Rep.finiteDimensional_coind_and_finrank_coind_eq_index_mul 0 below · cited by 2 · depth 15
• Restriction commutes with the cyclotomic twist of the dual Rep.finrank_invariants_res_dualTwist_eq 0 below · cited by 1 · depth 15
• The χ-twisted dual is an involution on finite-dimensional mod p representations Rep.nonempty_dualTwist_dualTwist_iso 0 below · cited by 1 · depth 15
• Smoothness of the twisted dual of a smooth representation Rep.dualTwist_smooth 1 below · cited by 6 · depth 16
• Equivariance of the evaluation pairing M × M^∨(χ) → k(χ) Rep.isEquivariantBilinear_eval_dualTwist 0 below · cited by 12 · depth 16
• Artin induction in characteristic p for additive invariants Rep.eq_zero_of_additive_of_forall_ind_isCyclic_coprime 15 below · cited by 1 · depth 17
• Inflated representations are smooth and unramified outside S Rep.res_quotient_fixingSubgroup_smooth_and_unramified 0 below · cited by 1 · depth 17
• Restriction along a group homomorphism is exact on Rep Rep.shortExact_map_resFunctor 0 below · cited by 8 · depth 17
• Additivity of ψ over disjoint unions of finite G-sets Rep.additive_tensor_ofMulAction_sigma 0 below · cited by 1 · depth 18
• Adjointness of the coinduced pairing under units and traces Rep.coind_pairing_adjoint 0 below · cited by 2 · depth 18
• Detection of additive invariants by cyclic p'-restrictions Rep.eq_of_additive_of_forall_nonempty_res_iso 8 below · cited by 2 · depth 18
• Deeper coinduction: inclusion scales the trace by [U:U'] Rep.exists_coind_inclusion_ker_trace 0 below · cited by 1 · depth 18
• Functoriality of coinduction, unit, shift and trace Rep.exists_coind_map_ker_trace 0 below · cited by 1 · depth 18
• Twisted duals reverse a short exact sequence of representations Rep.exists_dualTwist_shortExact 1 below · cited by 1 · depth 18
• Unit and trace for coind_S^Gres N, with composite [G:S] Rep.exists_hom_coind_res_comp_eq_index_smul 0 below · cited by 5 · depth 18
• Shift-minus-one operator on CoInd_U^GRes_U X Rep.exists_ker_trace_cyclicShift 0 below · cited by 1 · depth 18
• Coinduction from a finite-index subgroup multiplies dimension by the index Rep.finiteDimensional_coind_and_finrank_eq_index_mul 0 below · cited by 1 · depth 18
• Projection formula: Ind_D^GRes_D^G M ≅ M ⊗ k[G/D] Rep.nonempty_ind_res_iso_tensor_ofMulAction_quotient 0 below · cited by 1 · depth 18
• Degree-zero Shapiro: invariants of a coinduced representation Rep.nonempty_invariants_coind_equiv 0 below · cited by 1 · depth 18
• Degree-zero Shapiro lemma: (CoInd_S^G N)^G ≅ N^S Rep.nonempty_invariants_coind_linearEquiv_invariants 0 below · cited by 1 · depth 18
• Equivariant bijection transports restricted permutation-twisted modules Rep.nonempty_res_tensor_ofMulAction_iso_of_equiv 0 below · cited by 1 · depth 18
• Twisting by χ⁻¹ then by χ recovers a representation Rep.nonempty_twist_inv_twist_iso 0 below · cited by 1 · depth 18
• Exactness of coinduction from a finite-index subgroup and of its trace kernels Rep.shortExact_coind_ker_trace 0 below · cited by 1 · depth 18
• The order of G annihilates Tate cohomology in all degrees Rep.card_smul_eq_zero_of_tateCohomology 19 below · cited by 6 · depth 19
• Vanishing of δ on degree-zero classes from T.X₂ Rep.delta_hom_comp_eq_zero 0 below · cited by 1 · depth 19
• Detection of integer combinations by cyclic p'-subgroups Rep.eq_zero_of_forall_sum_mul_finrank_hom_res_eq_zero 4 below · cited by 1 · depth 19
• Coinduced restriction as functions on S/S'', diagonal action Rep.exists_coind_res_linearEquiv_quotient_fun 0 below · cited by 1 · depth 19
• Classes vanishing in H¹(G,Hom(R,X₂)) are connecting images Rep.exists_delta_hom_eq_of_map_ihom_map_eq_zero 0 below · cited by 1 · depth 19
• Lifting a morphism with vanishing connecting class Rep.exists_eq_comp_of_delta_hom_eq_zero 0 below · cited by 1 · depth 19
• Every map H¹(G,B)→ H²(G,C) factors through δ Rep.exists_hom_relationModuleInt_forall_map_delta_eq 124 below · cited by 2 · depth 19
• Additive functions on a pair of representations Rep.exists_isIrreducible_forall_additive_eq_sum 0 below · cited by 1 · depth 19
• Inflation of a vanishing Ext¹ relation-module class Rep.exists_preIota_eq_map_extInflR_zero_of_exists_preIota_eq_of_pit 0 below · cited by 2 · depth 19
• Lifting a relation-module map after restriction, cokernel form Rep.exists_resMap_comp_eq_comp_add_iota_comp_of_pit 0 below · cited by 1 · depth 19
• Additivity of dim Hom_H(T,-) in order prime to p Rep.finrank_hom_eq_add_of_shortExact_of_card_coprime 1 below · cited by 2 · depth 19
• Mackey decomposition for invariants of a coinduced representation Rep.finrank_invariants_res_coind_eq_finsum 0 below · cited by 1 · depth 19
• Invariants of a restricted representation depend only on the image Rep.invariants_res_eq_invariants_res_range 0 below · cited by 1 · depth 19
• Change of group commutes with φ_*∘δ in degree one Rep.map_delta_resMap_comp_eq_map_map_delta 0 below · cited by 2 · depth 19
• ℤ-freeness of the relation module carrier Rep.moduleFree_relationCarrier 0 below · cited by 6 · depth 19
• Restriction of a free representation to a subgroup is free Rep.nonempty_res_free_iso_free 0 below · cited by 6 · depth 19
• Twisting a representation is tensoring with a twisted trivial line Rep.nonempty_twist_iso_trivial_twist_tensor 0 below · cited by 1 · depth 19
• Exactness of the canonical free presentation over ℤ Rep.relationSeqInt_shortExact 0 below · cited by 4 · depth 19
• Hom(V,-) preserves short exactness for free V Rep.shortExact_map_ihom_of_free 0 below · cited by 1 · depth 19
• The order of G annihilates Tate ̂ H⁰ Rep.card_smul_eq_zero_of_tateH0 0 below · cited by 1 · depth 20
• Dévissage four-lemma for the degree-one duality dichotomy Rep.exists_comp_eq_or_exists_map_delta_ne_zero_of_devissage 0 below · cited by 1 · depth 20
• Extension dichotomy for maps from the integral relation module Rep.exists_comp_eq_or_exists_map_delta_ne_zero_of_forall_sum_rho_eq_nsmul 119 below · cited by 1 · depth 20
• Dévissage in degree two: extending φ along a presentation comparison Rep.exists_eq_comp_add_comp_of_forall_map_delta_eq_zero_of_shortExact_of_projective 119 below · cited by 1 · depth 20
• Embedding B into Ind_N^G B with p-torsion cokernel Rep.exists_hom_ind_injective_exact_of_forall_rho_eq 0 below · cited by 1 · depth 20
• Extension along Ind f₀ versus extension along f₀ Rep.exists_ind_map_comp_eq_iff_exists_comp_eq_homEquiv 0 below · cited by 1 · depth 20
• Semisimple trace decomposition over 𝔽ₚ in coprime order Rep.exists_isIrreducible_trace_eq_sum_of_card_coprime 0 below · cited by 1 · depth 20
• Existence of a cup product on Tate cohomology Rep.exists_isTateCupProduct 43 below · cited by 2 · depth 20
• Shapiro map compatible with corestriction and connecting maps Rep.exists_shapiro_corestriction_map_delta_ind_eq 4 below · cited by 1 · depth 20
• Vanishing of the Hom-defect map when pB=0 and φ(E)⊆ pE' Rep.extInflR_comp_homSeqTwo_g_eq_zero_of_forall_exists_eq_smul 0 below · cited by 1 · depth 20
• Finiteness of H¹ of the internal hom from a relation module Rep.finite_H1_ihom_relationModuleInt 23 below · cited by 1 · depth 20
• Linear independence of traces of pairwise non-isomorphic irreducibles Rep.forall_eq_zero_of_sum_mul_trace_eq_zero_of_isIrreducible 0 below · cited by 1 · depth 20
• Left exactness of Hom(-,E) on the free presentation Rep.homSeqOne_shortExact 0 below · cited by 2 · depth 20
• Tate acyclicity of Hom(ℤ[G]^{(B)},C) Rep.isZero_tateCohomology_ihom_free 5 below · cited by 2 · depth 20
• Restriction of a free representation is Tate-acyclic Rep.isZero_tateCohomology_res_free 10 below · cited by 2 · depth 20
• Finite generation of the relation module over ℤ Rep.moduleFinite_relationCarrier 0 below · cited by 3 · depth 20
• Tate ̂ H⁰ and ̂ H⁻¹ of a cyclic group on an additive model Rep.natCard_kerModRange_eq_natCard_tate_of_addEquiv 0 below · cited by 2 · depth 20
• Dimension shifting for Tate cohomology Rep.nonempty_tateCohomology_dimShiftUpObj_iso 14 below · cited by 2 · depth 20
• Dimension shifting down for Tate cohomology Rep.nonempty_tateCohomology_iso_dimShiftDownObj 12 below · cited by 3 · depth 20
• Induction along H≤ G preserves short exactness Rep.shortExact_map_indFunctor 0 below · cited by 1 · depth 20
• Dimension shifting: δⁿ is bijective for the sequence 0→ A''→ Ind A→ A→ 0 Rep.bijective_tateDelta_dimShiftDown 12 below · cited by 3 · depth 21
• Dimension shifting: δ is bijective for 0→ A→ Ind Res A→ A'→ 0 Rep.bijective_tateDelta_dimShiftUp 12 below · cited by 5 · depth 21
• Bijectivity of the Tate connecting map when the middle term vanishes Rep.bijective_tateDelta_of_isZero 8 below · cited by 15 · depth 21
• Exactness of the dimension-shift-down functor on short exact sequences Rep.dimShiftDownSC_shortExact 2 below · cited by 1 · depth 21
• The dimension-shifting-down sequence is short exact Rep.dimShiftDown_shortExact 1 below · cited by 11 · depth 21
• The dimension-shift sequence 0 → A → Ind₁^G A → A_* → 0 is short exact Rep.dimShiftUp_shortExact 3 below · cited by 8 · depth 21
• Norm-type relation maps extend over the free cover Rep.exists_relationModuleInt_iota_comp_eq_of_forall_hom_eq_sum_rho 0 below · cited by 1 · depth 21
• Mackey decomposition for coinduction from a normal subgroup Rep.exists_res_coind_linearEquiv_coind_comap 0 below · cited by 2 · depth 21
• Rank of H⁰(G,ℤ[X]) is the number of orbits Rep.finrank_groupCohomology_zero_ofMulAction 0 below · cited by 1 · depth 21
• Additivity of Γ-invariants of (-⊗ N) along a split short exact sequence Rep.finrank_invariants_tensor_eq_add_of_shortExact_of_trivial_of_coprime 1 below · cited by 2 · depth 21
• Vanishing of φ_*∘δ iff φ is a G-norm Rep.forall_map_delta_eq_zero_iff_exists_eq_sum_rho 117 below · cited by 2 · depth 21
• Induction from the trivial subgroup preserves short exactness Rep.indBotSC_shortExact 1 below · cited by 1 · depth 21
• The unit A → Ind_{mathbf 1}^GResA admits a k-linear retraction Rep.indBotr_indBotIota 2 below · cited by 7 · depth 21
• Tate cohomology of a free k[G]-module tensored with any representation vanishes Rep.isZero_tateCohomology_free_tensor 5 below · cited by 4 · depth 21
• Tate-acyclicity of Hom_k(Ind₁^G M, W) Rep.isZero_tateCohomology_ihom_indBot_trivial 4 below · cited by 2 · depth 21
• Tate cohomology of a module induced from the trivial subgroup vanishes Rep.isZero_tateCohomology_indBot 2 below · cited by 9 · depth 21
• Vanishing of Tate cohomology of Ind₁^GRes₁ A ⊗ B Rep.isZero_tateCohomology_indBot_tensor 5 below · cited by 6 · depth 21
• Vanishing of Tate cohomology passes to retracts Rep.isZero_tateCohomology_of_retract 2 below · cited by 2 · depth 21
• Nakayama–Tate: cohomological triviality from vanishing on p-subgroups Rep.isZero_tateCohomology_res_of_forall_isPGroup 33 below · cited by 3 · depth 21
• Tate cohomology of A ⊗ Ind₁^G B vanishes Rep.isZero_tateCohomology_tensor_indBot 6 below · cited by 5 · depth 21
• Maschke splitting for representations trivial on Λ Rep.nonempty_iso_biprod_of_shortExact_of_trivial_of_coprime 0 below · cited by 2 · depth 21
• Tate cohomology is invariant under isomorphism of representations Rep.nonempty_tateCohomology_iso_of_iso 0 below · cited by 12 · depth 21
• Tate dimension shifting along a Tate-acyclic extension Rep.nonempty_tateCohomology_iso_of_shortExact_of_isZero 6 below · cited by 5 · depth 21
• Shapiro's lemma in Tate degree 0 for subgroups Rep.nonempty_tateH0_coind_linearEquiv 0 below · cited by 2 · depth 21
• Shapiro's lemma in Tate degree -1 for coinduction Rep.nonempty_tateHneg1_coind_linearEquiv 0 below · cited by 2 · depth 21
• Equal marks force isomorphic mod p reductions Rep.nonempty_tensor_trivial_zmod_iso_of_finrank_invariants_eq 17 below · cited by 1 · depth 21
• Dimension shift down preserves A⊗- short exactness Rep.shortExact_dimShiftDownSC_map_tensorLeft 2 below · cited by 1 · depth 21
• Dimension shift down preserves ⊗ B-short exactness Rep.shortExact_dimShiftDownSC_map_tensorRight 2 below · cited by 1 · depth 21
• Tensoring the dimension-shift sequence with A preserves exactness Rep.shortExact_dimShiftDown_map_tensorLeft 3 below · cited by 5 · depth 21
• Dimension-shifting sequence remains short exact after -⊗ B Rep.shortExact_dimShiftDown_map_tensorRight 3 below · cited by 5 · depth 21
• Tensoring preserves short exactness of the Ind_{bot} shift Rep.shortExact_indBotSC_map_tensorLeft 1 below · cited by 1 · depth 21
• Tensoring the dimension-shift induction preserves short exactness Rep.shortExact_indBotSC_map_tensorRight 1 below · cited by 1 · depth 21
• Left tensoring by the dimension-shift subobject preserves short exactness Rep.shortExact_map_tensorLeft_dimShiftDownObj 2 below · cited by 1 · depth 21
• Induction from the trivial subgroup preserves tensor-exactness Rep.shortExact_map_tensorLeft_indBot 0 below · cited by 2 · depth 21
• Dimension-shift subobject preserves tensored short exactness Rep.shortExact_map_tensorRight_dimShiftDownObj 2 below · cited by 1 · depth 21
• Right tensoring with Ind₁^GRes₁ B preserves short exactness Rep.shortExact_map_tensorRight_indBot 0 below · cited by 2 · depth 21
• Right tensoring preserves k-split short exact sequences of G-representations Rep.shortExact_map_tensorRight_of_splitting 0 below · cited by 6 · depth 21
• Anticommutativity of Tate connecting maps in a 3× 3 diagram Rep.tateDelta_comp_tateDelta_eq_neg 0 below · cited by 1 · depth 21
• Anticommutation of Tate connecting maps in a 3× 3 diagram Rep.tateDelta_comp_tateDelta_eq_neg_of_hom 0 below · cited by 1 · depth 21
• Naturality of the Tate connecting maps in all degrees Rep.tateDelta_naturality 0 below · cited by 9 · depth 21
• Exactness of H₁(B)→ H₁(C)→ ̂ H⁻¹(A) at H₁(C) Rep.exact_map_tateDeltaNeg2 0 below · cited by 2 · depth 22
• Exactness of ̂ H⁰(C) → H¹(A) → H¹(B) Rep.exact_tateDelta0_map 0 below · cited by 2 · depth 22
• Exactness at ̂ H⁰(A) of the Tate sequence Rep.exact_tateDeltaNeg1_tateH0Map 0 below · cited by 2 · depth 22
• Exactness at ̂ H⁻¹ of the Tate sequence Rep.exact_tateDeltaNeg2_tateHneg1Map 0 below · cited by 2 · depth 22
• Exactness of the Tate long exact sequence at ̂ Hⁿ⁺¹(X₁) Rep.exact_tateDelta_tateMap 3 below · cited by 4 · depth 22
• Exactness of Tate ̂ H⁰ at the third term Rep.exact_tateH0Map_tateDelta0 0 below · cited by 2 · depth 22
• Exactness of the Tate sequence at ̂ H⁻¹ of the quotient Rep.exact_tateHneg1Map_tateDeltaNeg1 0 below · cited by 2 · depth 22
• Exactness of the Tate sequence at ̂ Hⁿ(X₃) Rep.exact_tateMap_tateDelta 3 below · cited by 3 · depth 22
• Commensurability of ℤ[G]-lattices with equal invariant ranks, G cyclic Rep.exists_hom_injective_finiteIndex_of_finrank_invariants_eq 6 below · cited by 1 · depth 22
• Conjugation data for the Mackey double coset formula Rep.exists_monoidHom_subgroupOf_conj_smul_and_hom_res_apply 0 below · cited by 1 · depth 22
• The unit A → Ind₁^GRes₁^G A as a sum over G Rep.indBotIota_apply 0 below · cited by 1 · depth 22
• Induced map on Ind_{{1}}^G generators Rep.indBotMap_indBotMk 0 below · cited by 6 · depth 22
• The augmentation Ind₁^G Res A → A admits a k-linear section Rep.indBotPi_indBotSigma 0 below · cited by 11 · depth 22
• Action on Ind₁^G Res₁^G A on elementary tensors Rep.indBot_rho_indBotMk 0 below · cited by 4 · depth 22
• Value of the retraction Ind₁^GRes A → A on generators Rep.indBotr_indBotMk 0 below · cited by 1 · depth 22
• Sylow reduction for vanishing of Tate cohomology Rep.isZero_tateCohomology_of_forall_sylow 25 below · cited by 2 · depth 22
• Vanishing of Tate cohomology of a p-group via consecutive degrees Rep.isZero_tateCohomology_of_isPGroup_of_forall 24 below · cited by 1 · depth 22
• Two-periodicity of Tate cohomology of a cyclic group Rep.nonempty_tateCohomology_iso_add_two 2 below · cited by 3 · depth 22
• Tate ̂ H⁰ and ̂ H⁻¹ of a cyclic group, elementwise Rep.nonempty_tate_addEquiv_elementwise 0 below · cited by 4 · depth 22
• Commensurable ℤ[G]-lattices have isomorphic mod p reductions Rep.nonempty_tensor_trivial_zmod_iso_of_injective_of_finiteIndex 0 below · cited by 1 · depth 22
• Left tensoring preserves k-linearly split short exact sequences Rep.shortExact_map_tensorLeft_of_splitting 0 below · cited by 6 · depth 22
• Tate ̂ H⁰ vanishes for modules induced from bot Rep.subsingleton_tateH0_ind_bot 0 below · cited by 1 · depth 22
• Vanishing of ̂ H⁻¹ for modules induced from the trivial subgroup Rep.subsingleton_tateHneg1_ind_bot 0 below · cited by 1 · depth 22
• Functoriality of Tate cohomology: compatibility with composition Rep.tateMap_comp 0 below · cited by 6 · depth 22
• Tate cohomology: the identity map induces the identity Rep.tateMap_id 0 below · cited by 6 · depth 22
• Short exactness of the augmentation sequence of k[G] Rep.augShortComplex_shortExact 0 below · cited by 1 · depth 23
• Commensurability of two G-lattices in a rational representation Rep.exists_hom_injective_finiteIndex_of_rat 0 below · cited by 1 · depth 23
• Finiteness of Tate cohomology for finitely generated ℤ[G]-coefficients Rep.finite_tateCohomology_of_moduleFinite 21 below · cited by 2 · depth 23
• Rank of lattice invariants equals dimension of rational invariants Rep.finrank_invariants_comp_eq_of_rat 0 below · cited by 1 · depth 23
• Vanishing of Tate cohomology when |G| acts bijectively Rep.isZero_tateCohomology_of_bijective_card_nsmul 23 below · cited by 3 · depth 23
• Tate cohomology of the trivial group vanishes Rep.isZero_tateCohomology_of_subsingleton 0 below · cited by 1 · depth 23
• Cohomological triviality of the splitting module in Tate's theorem Rep.isZero_tateCohomology_res_splittingModule 42 below · cited by 1 · depth 23
• Tensoring with a free ℤ-module preserves cohomological triviality Rep.isZero_tateCohomology_res_tensor_of_forall_isZero 47 below · cited by 1 · depth 23
• The Tate group ̂ H⁰(G,ℤ) has order |G| Rep.natCard_tateCohomology_zero_trivial_int 0 below · cited by 4 · depth 23
• Dimension shifting up commutes with restriction (Tate cohomology) Rep.nonempty_tateCohomology_res_dimShiftUpObj_iso_res 18 below · cited by 1 · depth 23
• Dimension shifting down, compatibly with restriction Rep.nonempty_tateCohomology_res_iso_res_dimShiftDownObj 16 below · cited by 4 · depth 23
• Tate ̂ H⁰ as homology of the norm–(g-1) complex Rep.nonempty_tateH0_linearEquiv_homology_normHomCompSub 0 below · cited by 1 · depth 23
• Tate ̂ H⁻¹ of a cyclic group as homology Rep.nonempty_tateHneg1_linearEquiv_homology_subCompNormHom 0 below · cited by 1 · depth 23
• Short exactness of the splitting sequence of a 2-cocycle Rep.splittingShortComplex_shortExact 0 below · cited by 2 · depth 23
• Fundamental class via two Tate connecting maps Rep.tateDelta_splitting_tateDelta_aug_eq_map_H2pi 0 below · cited by 1 · depth 23
• Corestriction after restriction is multiplication by the index on ̂ H⁰ Rep.tateH0Cores_comp_tateH0Res 0 below · cited by 1 · depth 23
• Cohomologically trivial G-modules have projective dimension at most one Rep.exists_shortExact_free_of_forall_isZero 43 below · cited by 1 · depth 24
• Tate-acyclicity of Hom(Ind₁^G A, W) Rep.isZero_tateCohomology_ihom_indBot 5 below · cited by 2 · depth 24
• Restriction to a finite subgroup of Ind₁^G is Tate-acyclic Rep.isZero_tateCohomology_res_indBot 5 below · cited by 2 · depth 24
• Image of [φ] in the splitting module vanishes Rep.map_splittingModuleIota_H2pi_eq_zero 0 below · cited by 1 · depth 24
• Tate degrees 0 and -1 match H² and H¹ for cyclic G Rep.natCard_tateCohomology_zero_and_neg_one_of_isCyclic 3 below · cited by 3 · depth 24
• Augmentation sequence is the dimension-shift sequence of k Rep.nonempty_augShortComplex_iso_dimShiftDown 2 below · cited by 1 · depth 24
• Cohomology of a restriction along an injective homomorphism Rep.nonempty_groupCohomology_res_iso_res_range 0 below · cited by 2 · depth 24
• Additivity of the Tate cohomology maps in the morphism Rep.tateMap_add 0 below · cited by 2 · depth 24
• Compatible pairings annihilate the sum of Tate connecting maps Rep.tateMap_tateDelta_add_tateMap_tateDelta_eq_zero 8 below · cited by 2 · depth 24
• Cohomologically trivial ℤ-free representations are retracts of free ones Rep.exists_retract_free_of_forall_isZero 38 below · cited by 1 · depth 25
• The map indBotπ sends [g⊗ a] to g⁻¹a Rep.indBotPi_indBotMk 0 below · cited by 2 · depth 25
• Mackey: Res_S Ind₁^G A ≅ Ind₁^S(bigoplus_{G/S}A) Rep.nonempty_res_indBot_iso 0 below · cited by 1 · depth 25
• Tate-acyclicity of Hom_ℤ(A,R) over a p-group Rep.isZero_tateCohomology_ihom_of_isPGroup 29 below · cited by 1 · depth 26
• Short exact sequences of representations split when H¹ of the internal Hom vanishes Rep.nonempty_splitting_of_isZero_H1_ihom 0 below · cited by 1 · depth 26
• Exactness of Tate cohomology functors on a short exact sequence Rep.exact_tateMap_tateMap 2 below · cited by 1 · depth 27
• Induced from the trivial subgroup when pV=0 and H₁ vanishes Rep.nonempty_iso_indBot_trivial_of_isPGroup 1 below · cited by 1 · depth 27
• Tate's theorem: shifting Tate cohomology by two Rep.nonempty_tateCohomology_trivial_iso_of_h1_h2 40 below · cited by 1 · depth 27
• Exactness of ̂ H⁰ at the middle term Rep.exact_tateH0Map_tateH0Map 0 below · cited by 1 · depth 28
• Exactness at the middle of Tate widehat H⁻¹ Rep.exact_tateHneg1Map_tateHneg1Map 0 below · cited by 1 · depth 28
• Splitting module: every H² class dies over the augmentation module Rep.exists_shortExact_map_two_eq_zero 2 below · cited by 1 · depth 28
• Dimension-shift kernel of the trivial module is the augmentation ideal Rep.exists_hom_dimShiftDownObj_trivial_leftRegular 1 below · cited by 1 · depth 29

Rep.IsTateCupProduct 18

• Cup product with a degree-zero class on the right Rep.IsTateCupProduct.cup_mk_right_eq_tateMap 31 below · cited by 3 · depth 20
• Tate–Nakayama surjectivity via a Tate-acyclic presentation Rep.IsTateCupProduct.exists_tateNakayamaPairing_right_eq_of_shortExact 102 below · cited by 1 · depth 20
• Tate–Nakayama pairing: surjectivity in the right variable Rep.IsTateCupProduct.exists_tateNakayamaPairing_right_eq 101 below · cited by 1 · depth 21
• Tate's theorem in cup-product form with free coefficients Rep.IsTateCupProduct.bijective_cup_of_h1_h2 79 below · cited by 2 · depth 22
• Associativity of the Tate cup product in all degrees Rep.IsTateCupProduct.cup_assoc 33 below · cited by 2 · depth 22
• Graded commutativity of the Tate cup product Rep.IsTateCupProduct.cup_comm 33 below · cited by 2 · depth 22
• Right surjectivity of the integral Tate duality pairing Rep.IsTateCupProduct.exists_cupEv_dual_right_eq 55 below · cited by 1 · depth 22
• Right non-degeneracy of Tate–Nakayama pairing after δ Rep.IsTateCupProduct.tateNakayamaPairing_right_eq_zero_of_shortExact 95 below · cited by 1 · depth 22
• Integral Tate duality via cup product, p+q=0 Rep.IsTateCupProduct.bijective_cupEv_dual_left 54 below · cited by 1 · depth 23
• Right non-degeneracy of the integral Tate pairing Rep.IsTateCupProduct.cupEv_dual_right_eq_zero 47 below · cited by 3 · depth 23
• Cup product with a degree-0 Tate class is an induced map Rep.IsTateCupProduct.cup_mk_left_eq_tateMap 31 below · cited by 2 · depth 23
• Cup product of invariant classes in degree (0,0) Rep.IsTateCupProduct.cup_mk_mk 32 below · cited by 2 · depth 23
• Injectivity of Tate duality pairing in all degrees Rep.IsTateCupProduct.injective_cupEv_characterDual 40 below · cited by 2 · depth 23
• Right non-degeneracy of the Tate–Nakayama pairing Rep.IsTateCupProduct.tateNakayamaPairing_right_eq_zero 94 below · cited by 1 · depth 23
• Right non-degeneracy of the Tate pairing against ℚ/ℤ Rep.IsTateCupProduct.cupEv_characterDual_eq_zero 40 below · cited by 1 · depth 24
• Left non-degeneracy of the Tate pairing in degrees (-1,0) Rep.IsTateCupProduct.injective_cupEv_negOne_characterDual 33 below · cited by 1 · depth 24
• Right non-degeneracy of the Tate pairing in degrees (-1,0) Rep.IsTateCupProduct.cupEv_characterDual_zero_eq_zero 33 below · cited by 1 · depth 25
• Cup product ̂ H⁻¹×̂ H⁰→̂ H⁻¹ on explicit classes Rep.IsTateCupProduct.cup_neg_one_mk 32 below · cited by 2 · depth 25