Main results 101 to 200
| Declaration | Kind | Where | Note |
|---|---|---|---|
ContinuousGroupCohomology.LevelCompact.compactZeroTateLimitπ_surjective |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 254 | |
ContinuousGroupCohomology.LevelCompact.compactUniversalNormSet |
def | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 262 | |
ContinuousGroupCohomology.LevelCompact.mem_finiteNorm_range_iff_relativeNorm_range |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 268 | |
ContinuousGroupCohomology.LevelCompact.mem_compactUniversalNormSet_iff |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 284 | |
ContinuousGroupCohomology.LevelCompact.compactTateLimitProjection_eq_zero_iff |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 309 | |
ContinuousGroupCohomology.LevelCompact.compactTateLimitNorm_range_eq_universalNormSet |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 340 | |
ContinuousGroupCohomology.LevelCompact.compactTateLimitProjection_eq_zero_iff_universalNorm |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 347 | |
ContinuousGroupCohomology.LevelCompact.compactTateLimitNorm_range_eq_universalNormSubmodule |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 355 | |
ContinuousGroupCohomology.LevelCompact.compactUniversalNormClosedSubgroup |
def | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 365 | |
ContinuousGroupCohomology.LevelCompact.compactUniversalNormClosedSubgroup_eq_ker |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 376 | |
ContinuousGroupCohomology.LevelCompact.compactTateUniversalNormQuotientEquiv |
def | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 386 | |
ContinuousGroupCohomology.LevelCompact.compactTateUniversalNormQuotientEquiv_mk |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 397 | |
ContinuousGroupCohomology.LevelCompact.compactTateUniversalNormQuotientEquiv_continuous |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 408 | |
ContinuousGroupCohomology.LevelCompact.compactTateUniversalNormQuotientIso |
def | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 423 | |
ContinuousGroupCohomology.LevelCompact.compactTateUniversalNormQuotientIso_mk |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 446 | |
ContinuousGroupCohomology.LevelCompactRep.compactFiniteCoinvariantsDiagramFunctor |
def | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 44 | |
ContinuousGroupCohomology.LevelCompactRep.compactFiniteCoinvariantsDiagramFunctor_obj |
theorem | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 64 | |
ContinuousGroupCohomology.LevelCompactRep.compactFiniteCoinvariantsDiagramFunctor_map_app |
theorem | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 69 | |
ContinuousGroupCohomology.LevelCompactRep.compactFiniteCoinvariantsLimitFunctor |
def | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 76 | |
ContinuousGroupCohomology.LevelCompactRep.compactFiniteCoinvariantsLimitFunctor_obj |
theorem | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 80 | |
ContinuousGroupCohomology.LevelCompactRep.compactFiniteCoinvariantsLimitFunctor_map_π |
theorem | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 86 | |
ContinuousGroupCohomology.LevelCompactRep.compactTotalInvariantsFunctor |
def | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 96 | |
ContinuousGroupCohomology.LevelCompactRep.compactTateLimitInclusion_naturality |
theorem | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 104 | |
ContinuousGroupCohomology.LevelCompactRep.compactTateLimitNorm_naturality |
theorem | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 132 | |
ContinuousGroupCohomology.LevelCompactRep.compactTateLimitProjection_naturality |
theorem | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 168 | |
ContinuousGroupCohomology.LevelCompactRep.compactTateLimitInclusionNat |
def | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 216 | |
ContinuousGroupCohomology.LevelCompactRep.compactTateLimitNormNat |
def | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 223 | |
ContinuousGroupCohomology.LevelCompactRep.compactTateLimitProjectionNat |
def | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 230 | |
ContinuousGroupCohomology.LevelCompactRep.groupMap_mem_compactUniversalNormClosedSubgroup |
theorem | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 238 | |
ContinuousGroupCohomology.LevelCompactRep.compactUniversalNormQuotientMap |
def | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 254 | |
ContinuousGroupCohomology.LevelCompactRep.compactUniversalNormQuotientMap_mk |
theorem | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 285 | |
ContinuousGroupCohomology.LevelCompactRep.compactUniversalNormQuotientMap_id |
theorem | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 292 | |
ContinuousGroupCohomology.LevelCompactRep.compactUniversalNormQuotientMap_comp |
theorem | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 304 | |
ContinuousGroupCohomology.LevelCompactRep.compactUniversalNormQuotientFunctor |
def | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 320 | |
ContinuousGroupCohomology.LevelCompactRep.compactTateUniversalNormQuotientIso_naturality |
theorem | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 331 | |
ContinuousGroupCohomology.LevelCompactRep.compactTateUniversalNormQuotientNatIso |
def | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 353 | |
ContinuousGroupCohomology.LevelCompactRep.compactTateUniversalNormQuotientNatIso_hom_app |
theorem | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 360 | |
ContinuousGroupCohomology.LevelCompactRep.compactTateUniversalNormQuotientNatIso_hom_app_mk |
theorem | ContinuousGroupCohomology/CompactTateNormNaturality.lean, line 366 | |
ContinuousGroupCohomology.RestrictedLevelCompactRep.fullNormLimit_projection_mem_iff |
theorem | ContinuousGroupCohomology/CompactUniversalNormLimits.lean, line 100 | |
ContinuousGroupCohomology.RestrictedLevelCompactRep.universalNorm_relativeNorm_surjective |
theorem | ContinuousGroupCohomology/CompactUniversalNormLimits.lean, line 121 | |
ContinuousGroupCohomology.RestrictedLevelCompactRep.fullInclusion |
def | ContinuousGroupCohomology/CompactUniversalNormLimits.lean, line 173 | |
ContinuousGroupCohomology.RestrictedLevelCompactRep.fullInclusion_apply |
theorem | ContinuousGroupCohomology/CompactUniversalNormLimits.lean, line 181 | |
ContinuousGroupCohomology.RestrictedLevelCompactRep.fullInclusion_limitMap_π |
theorem | ContinuousGroupCohomology/CompactUniversalNormLimits.lean, line 194 | |
ContinuousGroupCohomology.RestrictedLevelCompactRep.fullInclusion_limitMap_bijective |
theorem | ContinuousGroupCohomology/CompactUniversalNormLimits.lean, line 263 | |
ContinuousGroupCohomology.RestrictedLevelCompactRep.compactGroup_isIso_of_bijective |
theorem | ContinuousGroupCohomology/CompactUniversalNormLimits.lean, line 326 | |
ContinuousGroupCohomology.RestrictedLevelCompactRep.restrictedNormLimitIso |
def | ContinuousGroupCohomology/CompactUniversalNormLimits.lean, line 358 | |
ContinuousGroupCohomology.RestrictedLevelCompactRep.restrictedNormLimitIso_hom_π |
theorem | ContinuousGroupCohomology/CompactUniversalNormLimits.lean, line 367 | |
ContinuousGroupCohomology.RestrictedLevelCompactRep.restrictedNormLimitIso_inv_π |
theorem | ContinuousGroupCohomology/CompactUniversalNormLimits.lean, line 376 | |
ContinuousGroupCohomology.RestrictedLevelCompactRep.fullInclusion_naturality |
theorem | ContinuousGroupCohomology/CompactUniversalNormLimits.lean, line 395 | |
ContinuousGroupCohomology.RestrictedLevelCompactRep.restrictedNormLimitIso_naturality |
theorem | ContinuousGroupCohomology/CompactUniversalNormLimits.lean, line 407 | |
ContinuousGroupCohomology.RestrictedLevelCompactRep.universalNorm_limitIso_naturality |
theorem | ContinuousGroupCohomology/CompactUniversalNormLimits.lean, line 423 | |
TopRep.finiteSumCoind |
def | ContinuousGroupCohomology/FiniteAveraging.lean, line 33 | |
TopRep.finiteSumCoind_apply |
theorem | ContinuousGroupCohomology/FiniteAveraging.lean, line 48 | |
TopRep.coind₁ι_comp_finiteSumCoind |
theorem | ContinuousGroupCohomology/FiniteAveraging.lean, line 54 | |
TopRep.coind₁Map_comp_finiteSumCoind |
theorem | ContinuousGroupCohomology/FiniteAveraging.lean, line 65 | |
TopRep.finiteSumCoind_d_add_d_finiteSumCoind |
theorem | ContinuousGroupCohomology/FiniteAveraging.lean, line 77 | |
TopRep.finiteSumCochain |
def | ContinuousGroupCohomology/FiniteAveraging.lean, line 86 | |
TopRep.finiteSumCochain_comp_d_add_d_comp_finiteSumCochain |
theorem | ContinuousGroupCohomology/FiniteAveraging.lean, line 91 | |
TopModuleCat.shortComplex_homologyπ_surjective |
theorem | ContinuousGroupCohomology/FiniteAveraging.lean, line 111 | |
ContinuousCohomology.π_surjective |
theorem | ContinuousGroupCohomology/FiniteAveraging.lean, line 148 | |
ContinuousCohomology.finiteGroup_card_nsmul_π |
theorem | ContinuousGroupCohomology/FiniteAveraging.lean, line 155 | |
ContinuousCohomology.fintype_card_nsmul |
theorem | ContinuousGroupCohomology/FiniteAveraging.lean, line 197 | |
ContinuousCohomology.finiteGroup_card_nsmul |
theorem | ContinuousGroupCohomology/FiniteAveraging.lean, line 214 | |
ContinuousCohomology.finiteGroup_isAddTorsion |
theorem | ContinuousGroupCohomology/FiniteAveraging.lean, line 221 | |
TopRep.quotientInvariants_stable |
lemma | ContinuousGroupCohomology/QuotientInvariants.lean, line 37 | |
TopRep.quotientInvariantsAction |
def | ContinuousGroupCohomology/QuotientInvariants.lean, line 49 | |
TopRep.quotientInvariantsActionQuot |
def | ContinuousGroupCohomology/QuotientInvariants.lean, line 61 | |
TopRep.quotientInvariants |
def | ContinuousGroupCohomology/QuotientInvariants.lean, line 72 | |
TopRep.quotientInvariants_ρ_mk |
theorem | ContinuousGroupCohomology/QuotientInvariants.lean, line 76 | |
TopRep.quotientInvariantsIncl |
def | ContinuousGroupCohomology/QuotientInvariants.lean, line 83 | |
TopRep.quotientInvariantsMap |
def | ContinuousGroupCohomology/QuotientInvariants.lean, line 95 | |
TopRep.quotientInvariantsFunctor |
def | ContinuousGroupCohomology/QuotientInvariants.lean, line 109 | |
TopRep.quotientInvariantsFunctor_map_val |
theorem | ContinuousGroupCohomology/QuotientInvariants.lean, line 124 | |
TopRep.quotientInvariantsIncl_naturality |
theorem | ContinuousGroupCohomology/QuotientInvariants.lean, line 131 | |
TopRep.jointlyContinuous_quotientInvariants |
theorem | ContinuousGroupCohomology/QuotientInvariants.lean, line 140 | |
TopRep.jointlyContinuous_quotientInvariants_of_isOpen |
theorem | ContinuousGroupCohomology/QuotientInvariants.lean, line 169 | |
ContinuousMap.discreteTopology_of_compactSpace |
theorem | ContinuousGroupCohomology/Topology/ContinuousMap/CompactDiscrete.lean, line 27 | |
ContinuousMap.exists_openNormalSubgroup_factor |
theorem | ContinuousGroupCohomology/Topology/Algebra/CompactGroup/DiscreteFactor.lean, line 30 | |
ContinuousCohomology.resolutionMap_injective |
theorem | ContinuousGroupCohomology/CochainInjectivity.lean, line 39 | |
ContinuousCohomology.cochainsMap_injective |
theorem | ContinuousGroupCohomology/CochainInjectivity.lean, line 55 | |
ContinuousCohomology.cocyclesMap_injective |
theorem | ContinuousGroupCohomology/CochainInjectivity.lean, line 124 | |
ContinuousCohomology.cochainsMap_d_eq_zero_iff |
theorem | ContinuousGroupCohomology/CochainInjectivity.lean, line 136 | |
ContinuousCohomology.openNormalQuotientHom |
def | ContinuousGroupCohomology/ResolutionImage.lean, line 36 | |
ContinuousCohomology.StageDescends |
def | ContinuousGroupCohomology/ResolutionImage.lean, line 42 | |
ContinuousCohomology.stageDescends_zero |
theorem | ContinuousGroupCohomology/ResolutionImage.lean, line 49 | |
ContinuousCohomology.stageDescends_succ |
theorem | ContinuousGroupCohomology/ResolutionImage.lean, line 53 | |
ContinuousCohomology.stageDescends_antitone |
theorem | ContinuousGroupCohomology/ResolutionImage.lean, line 60 | |
ContinuousCohomology.stageDescends_iff_exists_lift |
theorem | ContinuousGroupCohomology/ResolutionImage.lean, line 77 | |
ContinuousCohomology.discreteTopology_resolutionX |
theorem | ContinuousGroupCohomology/FiniteStageResolution.lean, line 37 | |
ContinuousCohomology.exists_common_stage_refinement |
theorem | ContinuousGroupCohomology/FiniteStageResolution.lean, line 69 | |
ContinuousCohomology.exists_openNormal_stage_descends |
theorem | ContinuousGroupCohomology/FiniteStageResolution.lean, line 181 | |
ContinuousCohomology.exists_openNormal_resolution_lift |
theorem | ContinuousGroupCohomology/FiniteStageResolution.lean, line 209 | |
ContinuousCohomology.exists_openNormal_quotient_cochain_lift |
theorem | ContinuousGroupCohomology/FiniteStageCochains.lean, line 36 | |
ContinuousCohomology.exists_openNormal_quotient_closed_cochain_lift |
theorem | ContinuousGroupCohomology/FiniteStageCochains.lean, line 75 | |
ContinuousCohomology.exists_openNormal_quotient_class_lift |
theorem | ContinuousGroupCohomology/CompactDiscreteTorsion.lean, line 42 | |
ContinuousCohomology.exists_openNormal_quotient_card_nsmul_eq_zero |
theorem | ContinuousGroupCohomology/CompactDiscreteTorsion.lean, line 102 | |
ContinuousCohomology.compactDiscrete_isAddTorsion |
theorem | ContinuousGroupCohomology/CompactDiscreteTorsion.lean, line 117 | |
ContinuousCohomology.cochainsMap_exact_of_isEmbedding |
theorem | ContinuousGroupCohomology/CochainExactness.lean, line 160 | |
ContinuousMap.postcomp_exact_of_isInducing |
theorem | ContinuousGroupCohomology/Topology/ContinuousMap/Exact.lean, line 39 | |
ContinuousMap.postcomp_exact |
theorem | ContinuousGroupCohomology/Topology/ContinuousMap/Exact.lean, line 67 |
Quoted from the main results in formalization.yaml of FormalFrontier/continuous-group-cohomology at commit 4434e3f2, Apache-2.0.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.