Main results 1 to 100
| Declaration | Kind | Where | Note |
|---|---|---|---|
ContinuousCohomology.openNormalInflationCoconeIsColimit_type |
alias | ContinuousGroupCohomology/FiniteStageColimit.lean, line 194 | |
ContinuousCohomology.openNormalInflationCoconeIsColimit |
def | ContinuousGroupCohomology/FiniteStageColimit.lean, line 199 | |
ContinuousCohomology.discreteTopology_continuousCohomology |
theorem | ContinuousGroupCohomology/DiscreteCohomology.lean, line 58 | |
ContinuousCohomology.exists_quotient_cochain_lift_below |
theorem | ContinuousGroupCohomology/SeededCochains.lean, line 39 | |
TopModuleCat.shortComplex_homologyπ_eq_zero_iff |
theorem | ContinuousGroupCohomology/Algebra/Category/ModuleCat/Topology/HomologyBoundary.lean, line 31 | |
ContinuousCohomology.quotientTransitionHom |
def | ContinuousGroupCohomology/QuotientTransitions.lean, line 34 | |
ContinuousCohomology.quotientTransitionHom_mk |
theorem | ContinuousGroupCohomology/QuotientTransitions.lean, line 41 | |
ContinuousCohomology.quotientTransitionHom_surjective |
theorem | ContinuousGroupCohomology/QuotientTransitions.lean, line 46 | |
ContinuousCohomology.quotientTransitionHom_comp_quotient |
theorem | ContinuousGroupCohomology/QuotientTransitions.lean, line 52 | |
ContinuousCohomology.quotientTransitionHom_id |
theorem | ContinuousGroupCohomology/QuotientTransitions.lean, line 58 | |
ContinuousCohomology.quotientTransitionHom_comp |
theorem | ContinuousGroupCohomology/QuotientTransitions.lean, line 64 | |
ContinuousCohomology.quotientTransitionIncl |
def | ContinuousGroupCohomology/QuotientTransitions.lean, line 80 | |
ContinuousCohomology.quotientTransitionIncl_val |
theorem | ContinuousGroupCohomology/QuotientTransitions.lean, line 98 | |
ContinuousCohomology.quotientTransitionIncl_injective |
theorem | ContinuousGroupCohomology/QuotientTransitions.lean, line 102 | |
ContinuousCohomology.quotientTransitionIncl_inflate |
theorem | ContinuousGroupCohomology/QuotientTransitions.lean, line 112 | |
ContinuousCohomology.quotientTransition_cochainsMap_id |
theorem | ContinuousGroupCohomology/QuotientTransitions.lean, line 140 | |
ContinuousCohomology.quotientTransition_map_id |
theorem | ContinuousGroupCohomology/QuotientTransitions.lean, line 155 | |
ContinuousCohomology.quotientTransition_cochainsMap_comp |
theorem | ContinuousGroupCohomology/QuotientTransitions.lean, line 165 | |
ContinuousCohomology.quotientTransition_map_comp |
theorem | ContinuousGroupCohomology/QuotientTransitions.lean, line 185 | |
ContinuousCohomology.quotientTransition_cochainsMap_inflate |
theorem | ContinuousGroupCohomology/QuotientTransitions.lean, line 204 | |
ContinuousCohomology.quotientTransition_map_inflate |
theorem | ContinuousGroupCohomology/QuotientTransitions.lean, line 217 | |
ContinuousCohomology.class_eq_zero_of_inflation_zero_degree_zero |
theorem | ContinuousGroupCohomology/FiniteStageBoundary.lean, line 109 | |
ContinuousCohomology.exists_refinement_class_eq_zero |
theorem | ContinuousGroupCohomology/FiniteStageBoundary.lean, line 144 | |
ContinuousCohomology.exists_refinement_class_eq_of_inflation_eq |
theorem | ContinuousGroupCohomology/FiniteStageBoundary.lean, line 249 | |
ContinuousCohomology.isFiltered_orderDual_openNormalSubgroup |
theorem | ContinuousGroupCohomology/OpenNormalDiagram.lean, line 45 | |
ContinuousCohomology.openNormalCohomologyDiagram |
def | ContinuousGroupCohomology/OpenNormalDiagram.lean, line 312 | |
ContinuousCohomology.openNormalInflationCocone |
def | ContinuousGroupCohomology/OpenNormalDiagram.lean, line 325 | |
ContinuousCohomology.openNormalCohomologyDiagram_obj |
theorem | ContinuousGroupCohomology/OpenNormalDiagram.lean, line 335 | |
ContinuousCohomology.openNormalCohomologyDiagram_map |
theorem | ContinuousGroupCohomology/OpenNormalDiagram.lean, line 339 | |
ContinuousCohomology.openNormalInflationCocone_ι_app |
theorem | ContinuousGroupCohomology/OpenNormalDiagram.lean, line 345 | |
ContinuousCohomology.isAddTorsion_degreeOne |
theorem | ContinuousGroupCohomology/Torsion.lean, line 94 | |
ContinuousGroupCohomology.finiteNegativeOneDeflation_comp |
lemma | ContinuousGroupCohomology/FiniteDeflationTransitivity.lean, line 474 | |
CompHausAddCommGrp.FiniteBar.groupHomologyAddEquivPositive_naturality |
lemma | ContinuousGroupCohomology/CompactBarFunctoriality.lean, line 162 | |
ContinuousGroupCohomology.LevelCompact.tateCohomologyNegativeAddEquivFiniteTate |
def | ContinuousGroupCohomology/CompactNegativeTate.lean, line 439 | |
ContinuousGroupCohomology.LevelCompact.finiteTateNegOne |
abbrev | ContinuousGroupCohomology/FiniteTateTopology.lean, line 46 | |
ContinuousGroupCohomology.LevelCompact.finiteTateZero |
abbrev | ContinuousGroupCohomology/FiniteTateTopology.lean, line 53 | |
ContinuousGroupCohomology.LevelCompact.tateCohomologyNegOneAddEquivFiniteTate |
def | ContinuousGroupCohomology/FiniteTateTopology.lean, line 278 | |
ContinuousGroupCohomology.LevelCompact.tateCohomologyZeroAddEquivFiniteTate |
def | ContinuousGroupCohomology/FiniteTateTopology.lean, line 310 | |
ContinuousGroupCohomology.LevelCompact.finiteCoinvariantDeflation |
def | ContinuousGroupCohomology/FiniteCoinvariantDeflation.lean, line 44 | |
ContinuousGroupCohomology.LevelCompact.normFromFiniteCoinvariants_finiteCoinvariantDeflation |
lemma | ContinuousGroupCohomology/FiniteCoinvariantDeflation.lean, line 147 | |
ContinuousGroupCohomology.LevelCompact.finiteTateNegOneDeflation |
def | ContinuousGroupCohomology/ExceptionalTateDeflationTopology.lean, line 40 | |
ContinuousGroupCohomology.LevelCompact.finiteTateZeroDeflation |
def | ContinuousGroupCohomology/ExceptionalTateDeflationTopology.lean, line 53 | |
ContinuousGroupCohomology.LevelCompact.tateCohomologyNegOneAddEquivFiniteTate_finiteNegativeOneDeflation |
lemma | ContinuousGroupCohomology/ExceptionalTateDeflationTopology.lean, line 202 | |
ContinuousGroupCohomology.LevelCompact.tateCohomologyZeroAddEquivFiniteTate_finiteZeroDeflation |
lemma | ContinuousGroupCohomology/ExceptionalTateDeflationTopology.lean, line 247 | |
ContinuousGroupCohomology.LevelCompact.compactFiniteNegativeOneDeflationDiagram |
def | ContinuousGroupCohomology/CompactExceptionalTateDiagrams.lean, line 43 | |
ContinuousGroupCohomology.LevelCompact.compactFiniteZeroDeflationDiagram |
def | ContinuousGroupCohomology/CompactExceptionalTateDiagrams.lean, line 64 | |
ContinuousGroupCohomology.LevelCompact.finiteNegativeOneDeflationAdditiveDiagramIso |
def | ContinuousGroupCohomology/CompactExceptionalTateDiagrams.lean, line 85 | |
ContinuousGroupCohomology.LevelCompact.finiteZeroDeflationAdditiveDiagramIso |
def | ContinuousGroupCohomology/CompactExceptionalTateDiagrams.lean, line 104 | |
ContinuousGroupCohomology.LevelCompact.compactNegativeOneTateLimit |
abbrev | ContinuousGroupCohomology/CompactExceptionalTateLimits.lean, line 41 | |
ContinuousGroupCohomology.LevelCompact.compactNegativeOneTateLimitπ |
def | ContinuousGroupCohomology/CompactExceptionalTateLimits.lean, line 45 | |
ContinuousGroupCohomology.LevelCompact.compactNegativeOneTateLimitπ_naturality |
lemma | ContinuousGroupCohomology/CompactExceptionalTateLimits.lean, line 57 | |
ContinuousGroupCohomology.LevelCompact.compactNegativeOneTateLimitπ_range_eq_eventualRange |
lemma | ContinuousGroupCohomology/CompactExceptionalTateLimits.lean, line 65 | |
ContinuousGroupCohomology.LevelCompact.compactZeroTateLimit |
abbrev | ContinuousGroupCohomology/CompactExceptionalTateLimits.lean, line 74 | |
ContinuousGroupCohomology.LevelCompact.compactZeroTateLimitπ |
def | ContinuousGroupCohomology/CompactExceptionalTateLimits.lean, line 78 | |
ContinuousGroupCohomology.LevelCompact.compactZeroTateLimitπ_naturality |
lemma | ContinuousGroupCohomology/CompactExceptionalTateLimits.lean, line 90 | |
ContinuousGroupCohomology.LevelCompact.compactZeroTateLimitπ_range_eq_eventualRange |
lemma | ContinuousGroupCohomology/CompactExceptionalTateLimits.lean, line 98 | |
ContinuousGroupCohomology.LevelCompactRep.normFromFiniteCoinvariants_naturality_hom |
lemma | ContinuousGroupCohomology/CompactExceptionalTateCoefficientMaps.lean, line 182 | |
ContinuousGroupCohomology.LevelCompactRep.finiteTateNegOneMap_deflation |
lemma | ContinuousGroupCohomology/CompactExceptionalTateCoefficientMaps.lean, line 348 | |
ContinuousGroupCohomology.LevelCompactRep.finiteTateZeroMap_deflation |
lemma | ContinuousGroupCohomology/CompactExceptionalTateCoefficientMaps.lean, line 366 | |
ContinuousGroupCohomology.LevelCompactRep.compactNegativeOneTateLimitFunctor |
def | ContinuousGroupCohomology/CompactExceptionalTateLimitFunctoriality.lean, line 90 | |
ContinuousGroupCohomology.LevelCompactRep.compactZeroTateLimitFunctor |
def | ContinuousGroupCohomology/CompactExceptionalTateLimitFunctoriality.lean, line 95 | |
ContinuousGroupCohomology.LevelCompactRep.compactNegativeOneTateLimitFunctor_map_namedπ |
theorem | ContinuousGroupCohomology/CompactExceptionalTateLimitFunctoriality.lean, line 170 | |
ContinuousGroupCohomology.LevelCompactRep.compactZeroTateLimitFunctor_map_namedπ |
theorem | ContinuousGroupCohomology/CompactExceptionalTateLimitFunctoriality.lean, line 182 | |
ContinuousGroupCohomology.RestrictedLevelCompactRep.universalNormFunctor |
def | ContinuousGroupCohomology/RestrictedLevelCompactFunctoriality.lean, line 165 | |
ContinuousGroupCohomology.RestrictedLevelCompactRep.groupMap_relativeNorm |
theorem | ContinuousGroupCohomology/RestrictedLevelCompactFunctoriality.lean, line 293 | |
ContinuousGroupCohomology.RestrictedLevelCompactRep.restrictedNormDiagramFunctor |
def | ContinuousGroupCohomology/RestrictedLevelCompactFunctoriality.lean, line 367 | |
ContinuousGroupCohomology.LevelCompact.compactFiniteCoinvariantsDiagram |
def | ContinuousGroupCohomology/CompactFiniteTateNormSequence.lean, line 40 | |
ContinuousGroupCohomology.LevelCompact.compactTotalInvariantsDiagram |
def | ContinuousGroupCohomology/CompactFiniteTateNormSequence.lean, line 61 | |
ContinuousGroupCohomology.LevelCompact.compactFiniteTateNegOneInclusion |
def | ContinuousGroupCohomology/CompactFiniteTateNormSequence.lean, line 67 | |
ContinuousGroupCohomology.LevelCompact.compactFiniteTateNorm |
def | ContinuousGroupCohomology/CompactFiniteTateNormSequence.lean, line 80 | |
ContinuousGroupCohomology.LevelCompact.compactFiniteTateZeroProjection |
def | ContinuousGroupCohomology/CompactFiniteTateNormSequence.lean, line 93 | |
ContinuousGroupCohomology.LevelCompact.compactFiniteCoinvariantsDiagram_obj |
lemma | ContinuousGroupCohomology/CompactFiniteTateNormSequence.lean, line 106 | |
ContinuousGroupCohomology.LevelCompact.compactTotalInvariantsDiagram_obj |
lemma | ContinuousGroupCohomology/CompactFiniteTateNormSequence.lean, line 111 | |
ContinuousGroupCohomology.LevelCompact.compactFiniteTateNegOneInclusion_app |
lemma | ContinuousGroupCohomology/CompactFiniteTateNormSequence.lean, line 116 | |
ContinuousGroupCohomology.LevelCompact.compactFiniteTateNorm_app |
lemma | ContinuousGroupCohomology/CompactFiniteTateNormSequence.lean, line 121 | |
ContinuousGroupCohomology.LevelCompact.compactFiniteTateZeroProjection_app |
lemma | ContinuousGroupCohomology/CompactFiniteTateNormSequence.lean, line 126 | |
ContinuousGroupCohomology.LevelCompact.finiteTateNorm_exact_left |
theorem | ContinuousGroupCohomology/CompactFiniteTateNormSequence.lean, line 131 | |
ContinuousGroupCohomology.LevelCompact.finiteTateNorm_exact_right |
theorem | ContinuousGroupCohomology/CompactFiniteTateNormSequence.lean, line 143 | |
ContinuousGroupCohomology.LevelCompact.finiteTateNegOneι_injective |
theorem | ContinuousGroupCohomology/CompactFiniteTateNormSequence.lean, line 157 | |
ContinuousGroupCohomology.LevelCompact.finiteTateZeroπ_surjective |
theorem | ContinuousGroupCohomology/CompactFiniteTateNormSequence.lean, line 163 | |
ContinuousGroupCohomology.LevelCompact.finiteTateZeroDeflation_surjective |
theorem | ContinuousGroupCohomology/CompactFiniteTateNormSequence.lean, line 171 | |
ContinuousGroupCohomology.LevelCompact.fullOpenNormalSubgroup |
def | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 40 | |
ContinuousGroupCohomology.LevelCompact.fullOpenNormalSubgroup_toOpenSubgroup |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 43 | |
ContinuousGroupCohomology.LevelCompact.le_fullOpenNormalSubgroup |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 46 | |
ContinuousGroupCohomology.LevelCompact.relativeNorm_fullOpenNormalSubgroup |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 52 | |
ContinuousGroupCohomology.LevelCompact.compactFiniteCoinvariantsLimit |
abbrev | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 66 | |
ContinuousGroupCohomology.LevelCompact.compactTotalInvariantsCone |
def | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 70 | |
ContinuousGroupCohomology.LevelCompact.compactTotalInvariantsCone_isLimit |
alias | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 80 | |
ContinuousGroupCohomology.LevelCompact.compactTotalInvariantsLimitIso |
def | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 83 | |
ContinuousGroupCohomology.LevelCompact.compactTotalInvariantsLimitIso_hom |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 90 | |
ContinuousGroupCohomology.LevelCompact.compactTateLimitInclusion |
def | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 99 | |
ContinuousGroupCohomology.LevelCompact.compactTateLimitNorm |
def | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 104 | |
ContinuousGroupCohomology.LevelCompact.compactTateLimitProjection |
def | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 110 | |
ContinuousGroupCohomology.LevelCompact.compactTateLimitInclusion_π |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 115 | |
ContinuousGroupCohomology.LevelCompact.compactTateLimitNorm_π |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 122 | |
ContinuousGroupCohomology.LevelCompact.compactTateLimitProjection_π |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 134 | |
ContinuousGroupCohomology.LevelCompact.compactTateLimit_exact_left |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 148 | |
ContinuousGroupCohomology.LevelCompact.compactTateLimit_exact_right |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 174 | |
ContinuousGroupCohomology.LevelCompact.compactTateLimitInclusion_injective |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 218 | |
ContinuousGroupCohomology.LevelCompact.compactTateLimitProjection_surjective |
theorem | ContinuousGroupCohomology/CompactTateNormLimitSequence.lean, line 238 |
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.