Res

📁 Source: Mathlib/RepresentationTheory/Rep/Res.lean

Statistics

Metric	Count
Definitions liftHomOfSurj, ofQuotient, res, resFunctor, resOfQuotientIso	5
Theorems coe_res_obj_ρ', full_res, instAdditiveResFunctor, instFaithfulResFunctor, instLinearResFunctor, liftHomOfSurj_toLinearMap, res_map_hom_toLinearMap, res_obj_V, res_obj_ρ	9
Total	14

Rep

Definitions

Name	Category	Theorems
liftHomOfSurj 📖	CompOp	1 math math: liftHomOfSurj_toLinearMap
ofQuotient 📖	CompOp	4 math math: groupHomology.map₁_quotientGroupMk'_epi, groupHomology.H1CoresCoinfOfTrivial_g, groupHomology.H1CoresCoinfOfTrivial_X₃, groupHomology.mapCycles₁_quotientGroupMk'_epi
res 📖	CompOp	129 math math: groupHomology.mapCycles₂_comp_assoc, groupHomology.map₁_quotientGroupMk'_epi, groupCohomology.cocyclesMap_id_comp_assoc, coindResAdjunction_counit_app, groupHomology.chainsMap_f_3_comp_chainsIso₃_apply, resCoindToHom_hom_apply_coe, groupHomology.mapCycles₁_comp_apply, groupHomology.mapShortComplexH1_zero, groupHomology.cyclesMap_id_comp, groupHomology.mapShortComplexH2_zero, groupHomology.comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top, groupHomology.mapCycles₁_comp_assoc, groupHomology.H0π_comp_map, groupCohomology.cochainsMap_comp, groupHomology.coresNatTrans_app, groupCohomology.map_H0Iso_hom_f_apply, groupCohomology.congr, groupHomology.H1CoresCoinfOfTrivial_X₁, groupCohomology.mapShortComplexH2_comp_assoc, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply, groupCohomology.mapCocycles₂_comp_i_apply, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_apply, groupHomology.mapCycles₁_id_comp_assoc, groupHomology.mapCycles₁_comp, groupHomology.map_comp, groupCohomology.map_comp, groupHomology.map_id_comp, coinvariantsTensorIndIso_inv, coindVEquiv_symm_apply_coe, liftHomOfSurj_toLinearMap, groupHomology.H1CoresCoinf_X₁, groupHomology.mapCycles₂_id_comp, groupHomology.cyclesMap_comp_assoc, groupHomology.cyclesMap_comp_cyclesIso₀_hom_apply, groupHomology.chainsMap_f_single, coindFunctorIso_inv_app_hom_toFun_coe, coinvariantsTensorIndIso_hom, groupCohomology.map_H0Iso_hom_f, groupCohomology.cochainsMap_zero, groupHomology.map_comp_assoc, groupHomology.mapCycles₁_id_comp_apply, groupCohomology.cochainsMap_id_comp, groupCohomology.mapShortComplexH2_comp, groupCohomology.cochainsMap_comp_assoc, groupHomology.mapCycles₁_comp_i_apply, groupHomology.mapCycles₂_comp, groupHomology.cyclesIso₀_inv_comp_cyclesMap_apply, resIndAdjunction_homEquiv_symm_apply, groupHomology.H0π_comp_map_assoc, groupCohomology.H1InfRes_X₃, groupCohomology.cocyclesMap_comp, groupCohomology.resNatTrans_app, groupCohomology.mapShortComplexH2_zero, resIndAdjunction_homEquiv_apply, groupHomology.mapCycles₂_comp_apply, resCoindHomEquiv_symm_apply, groupHomology.chainsMap_id_comp, groupHomology.mapShortComplexH1_id_comp, groupHomology.mapShortComplexH1_comp, coindResAdjunction_homEquiv_apply, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_assoc, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply, coindVEquiv_apply, Representation.coind'_apply_apply, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply, groupCohomology.mapShortComplexH2_id_comp_assoc, groupHomology.mapCycles₂_id_comp_assoc, groupHomology.mapShortComplexH2_comp, groupHomology.mapCycles₁_id_comp, groupHomology.lsingle_comp_chainsMap_f, coe_res_obj_ρ', groupHomology.cyclesMap_comp_cyclesIso₀_hom, groupCohomology.cochainsMap_f, coind'_ext_iff, groupHomology.chainsMap_comp, groupCohomology.map_id_comp_assoc, groupHomology.chainsMap_f_0_comp_chainsIso₀_assoc, groupHomology.congr, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f, groupCohomology.H1InfRes_g, groupCohomology.mapShortComplexH1_id_comp, groupCohomology.cocyclesMap_comp_assoc, coindResAdjunction_homEquiv_symm_apply, groupCohomology.mapShortComplexH1_comp, groupHomology.cyclesIso₀_inv_comp_cyclesMap_assoc, groupCohomology.map_id_comp, indResHomEquiv_apply, groupHomology.chainsMap_f_hom, resCoindHomEquiv_apply, groupHomology.H1CoresCoinfOfTrivial_f, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀, groupCohomology.mapCocycles₁_comp_i_apply, groupHomology.mapCycles₂_id_comp_apply, groupCohomology.cochainsMap_f_hom, groupHomology.H1CoresCoinfOfTrivial_g, groupCohomology.mapShortComplexH1_id_comp_assoc, groupCohomology.mapShortComplexH1_zero, groupCohomology.mapShortComplexH1_comp_assoc, groupHomology.cyclesIso₀_inv_comp_cyclesMap, groupCohomology.mapShortComplexH2_id_comp, resIndAdjunction_unit_app, coinvariantsTensorIndHom_mk_tmul_indVMk, groupHomology.chainsMap_zero, groupHomology.mapShortComplexH2_id_comp, indResHomEquiv_symm_apply, groupHomology.mapCycles₂_comp_i_apply, groupCohomology.cocyclesMap_id_comp, res_obj_ρ, groupHomology.chainsMap_f_0_comp_chainsIso₀_apply, groupHomology.cyclesMap_comp, groupHomology.mapShortComplexH1_τ₃, groupHomology.cyclesMap_comp_cyclesIso₀_hom_assoc, groupHomology.lsingle_comp_chainsMap_f_assoc, groupHomology.H1CoresCoinf_f, groupCohomology.cochainsMap_id_comp_assoc, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_assoc, groupCohomology.map_H0Iso_hom_f_assoc, coinvariantsTensorIndInv_mk_tmul_indMk, groupHomology.chainsMap_f_1_comp_chainsIso₁_apply, groupHomology.mapCycles₁_quotientGroupMk'_epi, groupHomology.H0π_comp_map_apply, groupCohomology.mapShortComplexH1_τ₁, res_obj_V, groupHomology.chainsMap_f_0_comp_chainsIso₀, groupHomology.chainsMap_f, groupHomology.chainsMap_f_2_comp_chainsIso₂_apply, groupCohomology.map_comp_assoc, coindFunctorIso_hom_app_hom_toFun_hom_toFun
resFunctor 📖	CompOp	33 math math: coindResAdjunction_counit_app, full_res, instAdditiveResFunctor, groupCohomology.cochainsMap_comp, groupHomology.coresNatTrans_app, groupHomology.mapCycles₁_comp, groupHomology.map_comp, groupCohomology.map_comp, coinvariantsTensorIndNatIso_inv_app, res_map_hom_toLinearMap, coindResAdjunction_unit_app, groupCohomology.mapShortComplexH2_comp, instIsRightAdjointResFunctor, groupHomology.mapCycles₂_comp, resIndAdjunction_homEquiv_symm_apply, groupCohomology.cocyclesMap_comp, groupCohomology.resNatTrans_app, resIndAdjunction_homEquiv_apply, groupHomology.mapShortComplexH1_comp, coindResAdjunction_homEquiv_apply, resIndAdjunction_counit_app, instLinearResFunctor, Representation.coind'_apply_apply, groupHomology.mapShortComplexH2_comp, groupHomology.chainsMap_comp, coinvariantsTensorIndNatIso_hom_app, coindResAdjunction_homEquiv_symm_apply, groupCohomology.mapShortComplexH1_comp, instPreservesProjectiveObjectsSubtypeMemSubgroupResFunctorSubtype, instIsLeftAdjointResFunctor, resIndAdjunction_unit_app, groupHomology.cyclesMap_comp, instFaithfulResFunctor
resOfQuotientIso 📖	CompOp	3 math math: groupHomology.map₁_quotientGroupMk'_epi, groupHomology.H1CoresCoinfOfTrivial_g, groupHomology.mapCycles₁_quotientGroupMk'_epi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_res_obj_ρ' 📖	mathematical	—	DFunLike.coe Representation V CommSemiring.toSemiring CommRing.toCommSemiring res AddCommGroup.toAddCommMonoid hV1 hV2 LinearMap RingHom.id Semiring.toNonAssocSemiring MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ MonoidHom	—	—
full_res 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	CategoryTheory.Functor.Full Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory resFunctor	—	hom_ext Representation.IntertwiningMap.ext res_map_hom_toLinearMap liftHomOfSurj_toLinearMap
instAdditiveResFunctor 📖	mathematical	—	CategoryTheory.Functor.Additive Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory instPreadditive resFunctor	—	hom_ext Representation.IntertwiningMap.ext RingHomCompTriple.ids
instFaithfulResFunctor 📖	mathematical	—	CategoryTheory.Functor.Faithful Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory resFunctor	—	hom_ext Representation.IntertwiningMap.ext Representation.IntertwiningMap.ext_iff hom_ext_iff
instLinearResFunctor 📖	mathematical	—	CategoryTheory.Functor.Linear CommSemiring.toSemiring CommRing.toCommSemiring Rep instCategory instPreadditive instLinear resFunctor	—	hom_ext Representation.IntertwiningMap.ext smul_hom smulCommClass_self Representation.IntertwiningMap.toLinearMap_smul res_map_hom_toLinearMap
liftHomOfSurj_toLinearMap 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	Representation.IntertwiningMap.toLinearMap V CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid hV1 hV2 ρ Hom.hom liftHomOfSurj res	—	—
res_map_hom_toLinearMap 📖	mathematical	—	Representation.IntertwiningMap.toLinearMap V CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Functor.obj Rep instCategory resFunctor AddCommGroup.toAddCommMonoid hV1 hV2 ρ Hom.hom CategoryTheory.Functor.map	—	—
res_obj_V 📖	mathematical	—	V CommSemiring.toSemiring CommRing.toCommSemiring res	—	—
res_obj_ρ 📖	mathematical	—	ρ CommSemiring.toSemiring CommRing.toCommSemiring res MonoidHom.comp LinearMap RingHom.id Semiring.toNonAssocSemiring V AddCommGroup.toAddCommMonoid hV1 hV2 MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	—

---

← Back to Index