`OAI/GroupTheory/PolycyclicRecognition/Finiteness/`

1218 declarations, 0 contain sorry, 0 declared as axioms; 267 files

Files

AbelianCyclicFinitenessEndgame.lean 2 declarations
AbelianMultilinearHomology.lean 2 declarations
AbelianNormalExteriorFiniteness.lean 7 declarations
AbelianNormalFinitenessEndgame.lean 1 declarations
AbelianNormalHigherExteriorFiniteness.lean 6 declarations
AbelianReducedCohomology.lean 2 declarations
AbelianSecondHomologyNaturality.lean 3 declarations
AbelianSecondHomologyPairing.lean 10 declarations
AbelianizationMonoidFiniteness.lean 5 declarations
AscendingFinitenessEndgame.lean 4 declarations
AutomorphismSecondHomologyAction.lean 4 declarations
BicomplexDiagonal.lean 9 declarations
BicomplexDiagonalComponents.lean 5 declarations
BicomplexDiagonalCycles.lean 7 declarations
BicomplexDiagonalDifferential.lean 8 declarations
BicomplexDiagonalNaturality.lean 3 declarations
BicomplexFilteredHomology.lean 9 declarations
BicomplexFiniteElimination.lean 5 declarations
BicomplexFiniteHomology.lean 5 declarations
BicomplexHorizontalBoundary.lean 8 declarations
BicomplexRowHomology.lean 4 declarations
BicomplexSecondPageCycles.lean 5 declarations
BicomplexSecondPageFiniteness.lean 2 declarations
BicomplexSecondPageVanishing.lean 2 declarations
BicomplexTotalComparison.lean 3 declarations
BicomplexTotalExact.lean 7 declarations
BicomplexTotalExactFunctor.lean 4 declarations
BicomplexZeroRows.lean 4 declarations
BilateralCochainShift.lean 7 declarations
BooleanStepProjective.lean 7 declarations
BoundedResolutionTopHomology.lean 1 declarations
CartanReducedCohomology.lean 1 declarations
CartanVanishingHeight.lean 1 declarations
CayleyPoincare.lean 3 declarations
CentralCocycleHomology.lean 7 declarations
CentralQuotientVanishing.lean 1 declarations
CentralTransgressionHomologyExact.lean 2 declarations
ChosenIntegralResolution.lean 15 declarations
CoarseFiniteness.lean 2 declarations
CoarseGroupRingCohomology.lean 5 declarations
CoarsePoincareDuality.lean 1 declarations
CochainExhaustion.lean 4 declarations
CochainSuccessor.lean 14 declarations
CoefficientNaturalCohomology.lean 4 declarations
CoefficientNormalHomology.lean 7 declarations
CoefficientResolutionHomology.lean 7 declarations
CofiberChainHomology.lean 1 declarations
CofiberCochainSequence.lean 12 declarations
CofiberCohomology.lean 5 declarations
CofiberResolution.lean 3 declarations
CohomologicalFiniteness.lean 11 declarations
CokernelResolution.lean 7 declarations
CompleteCohomologyConnecting.lean 7 declarations
CompleteCohomologyFiniteResolution.lean 2 declarations
CompleteCohomologyLongExact.lean 6 declarations
CompleteCohomologyMiddleExact.lean 2 declarations
CompleteCohomologyStableMaps.lean 7 declarations
CompleteVanishingExactFunctor.lean 4 declarations
CompletedCohomology.lean 12 declarations
CompletedCohomologyAdditive.lean 3 declarations
CompletedCohomologyColimitKernel.lean 2 declarations
CompletedCohomologyColimitSurjectivity.lean 2 declarations
CompletedCohomologyFinitary.lean 1 declarations
CompletedCohomologyProjective.lean 7 declarations
CompletedIdentity.lean 7 declarations
CompletedIdentityTorsion.lean 3 declarations
ConjugationCochains.lean 7 declarations
ControlledCochainComplex.lean 6 declarations
ControlledCochainHomotopy.lean 3 declarations
ControlledCochainMap.lean 3 declarations
ControlledCochains.lean 8 declarations
ControlledFillingsFromResolution.lean 2 declarations
ControlledGroupCohomology.lean 4 declarations
ControlledTupleMaps.lean 3 declarations
CountableSumVanishing.lean 9 declarations
CountableUnionCohomology.lean 4 declarations
CyclicDuality.lean 3 declarations
CyclicExtensionFiniteness.lean 3 declarations
CyclicInvariantTopHomology.lean 2 declarations
CyclicKernelHomologyFiniteness.lean 1 declarations
CyclicTopHomologyInjection.lean 3 declarations
DimensionFromRegularCohomology.lean 7 declarations
DualityEndgame.lean 5 declarations
ExteriorSquareHomology.lean 3 declarations
ExteriorSquareHomologyNaturality.lean 6 declarations
FiniteAugmentationFromFP.lean 1 declarations
FiniteAugmentationKernel.lean 5 declarations
FiniteDimensionCohomology.lean 4 declarations
FiniteDimensionHomology.lean 1 declarations
FiniteGroupProjectiveNorm.lean 5 declarations
FiniteGroupSyzygyScalar.lean 5 declarations
FiniteIndexFiniteness.lean 4 declarations
FiniteIndexHomologyDegree.lean 2 declarations
FiniteIndexTopHomology.lean 4 declarations
FiniteIntegralHomology.lean 3 declarations
FiniteKernelsFromFillings.lean 2 declarations
FinitePresentationSequentialLimit.lean 3 declarations
FinitePresentationSyzygies.lean 4 declarations
FiniteProjectivePresentations.lean 5 declarations
FiniteResolutionTruncation.lean 15 declarations
FiniteStabilizerSumVanishing.lean 3 declarations
FiniteSumCompleteVanishing.lean 4 declarations
FinitenessFromControlledFillings.lean 2 declarations
FinsuppCohomology.lean 3 declarations
FinsuppCompleteVanishing.lean 2 declarations
FirstHomologyAbelianizationNaturality.lean 4 declarations
FreeAbelianDuality.lean 8 declarations
FreeRightCoefficientHomology.lean 5 declarations
GroupIsoDuality.lean 2 declarations
GroupIsoFiniteness.lean 1 declarations
HeightKernelCoefficientDimension.lean 2 declarations
HomogeneousCochainCoordinates.lean 5 declarations
HomogeneousRepresentationCochains.lean 13 declarations
HomologyBoundTransport.lean 1 declarations
HomologyBoundary.lean 2 declarations
HomologyClassExhaustion.lean 6 declarations
HomologyCoefficientLinearity.lean 2 declarations
HomologyExhaustion.lean 2 declarations
HomologyExhaustionFiniteness.lean 3 declarations
HomologyExhaustionInjectivity.lean 3 declarations
HomologyOrientationEquiv.lean 3 declarations
HomologyRankOneLimit.lean 4 declarations
HorseshoeProjectiveTowers.lean 8 declarations
HorseshoeSyzygySequence.lean 6 declarations
InducedBarHomology.lean 5 declarations
InducedCohomologyDifference.lean 5 declarations
InducedFiniteRationalVanishing.lean 2 declarations
InducedResolutionHomology.lean 7 declarations
InducedTranslationAugmentation.lean 7 declarations
InducedTranslationCochains.lean 2 declarations
InductionCochains.lean 2 declarations
InductionExhaustionVanishing.lean 4 declarations
InfiniteCyclicDuality.lean 13 declarations
InfiniteCyclicFiniteness.lean 5 declarations
InfiniteCyclicResolution.lean 11 declarations
InfiniteQuotientHomology.lean 2 declarations
InnerHomologyAction.lean 3 declarations
IntegerExtensionDuality.lean 7 declarations
IntegerExtensionHomology.lean 2 declarations
IntegerExtensionHomologyBound.lean 1 declarations
IntegerInducedCochains.lean 5 declarations
IntegerProjectiveCoefficientDimension.lean 2 declarations
IntegralAugmentation.lean 6 declarations
IntegralBarAugmentation.lean 8 declarations
IntegralProjectiveTower.lean 12 declarations
IteratedCoinvariantsHomology.lean 4 declarations
LatticeDualityComparison.lean 2 declarations
LatticeExtensionHomologyBound.lean 2 declarations
LatticeKernelHomologyFiniteness.lean 1 declarations
LatticeTopHomologyInjection.lean 1 declarations
LiDualityFromFiniteness.lean 1 declarations
LocalInductionVanishing.lean 3 declarations
LocalVirtualPolycyclicVanishing.lean 4 declarations
LocallyFiniteCoefficientHomology.lean 6 declarations
LocallyFiniteRationalHomology.lean 3 declarations
NestedNormalHomology.lean 4 declarations
NilpotentAbelianFiniteness.lean 3 declarations
NilpotentCyclicDuality.lean 2 declarations
NilpotentFirstHomologyDimension.lean 4 declarations
NilpotentLatticeDuality.lean 1 declarations
NilpotentLatticeFiniteness.lean 2 declarations
NilpotentNormalRationalHomology.lean 3 declarations
NilpotentReducedCohomology.lean 2 declarations
NilpotentStageTopHomology.lean 1 declarations
NilpotentTopHomologyFiniteness.lean 1 declarations
NoetherianResolutionHomology.lean 3 declarations
NormalCentralHomologyExact.lean 5 declarations
NormalCoinvariantsProjective.lean 5 declarations
NormalDerivedHomologyFiniteness.lean 4 declarations
NormalExtensionBicomplex.lean 5 declarations
NormalExtensionColumnHomology.lean 5 declarations
NormalExtensionHomologyFiniteness.lean 1 declarations
NormalExtensionHomologyVanishing.lean 2 declarations
NormalExtensionTotalHomology.lean 2 declarations
NormalFirstHomologyAbelianization.lean 2 declarations
NormalHomologyAction.lean 5 declarations
NormalHomologyActionComparison.lean 5 declarations
NormalHomologyModuleFiniteness.lean 5 declarations
NormalHomologyQuotient.lean 2 declarations
NormalInductionDimension.lean 4 declarations
NormalQuotientCompleteVanishing.lean 8 declarations
NormalizedProjectiveResolution.lean 12 declarations
NormalizedProjectiveTower.lean 8 declarations
NormalizedResolutionSyzygies.lean 6 declarations
NormalizedStableSyzygyMap.lean 7 declarations
NormalizedSyzygyColimit.lean 3 declarations
NormalizedSyzygyFunctor.lean 10 declarations
NormalizedSyzygyIteration.lean 4 declarations
OrientationHomologyAction.lean 6 declarations
PoincareDualityBase.lean 5 declarations
PoincareHomologyDimension.lean 1 declarations
PoincareTopHomology.lean 1 declarations
PolyZDuality.lean 4 declarations
PolyZResolution.lean 3 declarations
PolycyclicDualityComparison.lean 5 declarations
ProjectiveCoefficientHomology.lean 4 declarations
ProjectiveKernelStableMap.lean 4 declarations
ProjectivePresentationComparison.lean 1 declarations
ProjectiveResolutionSyzygies.lean 6 declarations
ProjectiveTensorCoefficient.lean 2 declarations
ProjectiveTowerCohomology.lean 11 declarations
ProjectiveTowerComparison.lean 4 declarations
ProjectiveTowerDimension.lean 2 declarations
ProjectiveTowerExactness.lean 1 declarations
QuotientCoinvariantsFiniteness.lean 6 declarations
QuotientResolutionHomology.lean 3 declarations
RankOneKernelFiniteness.lean 1 declarations
RationalAcyclicKernelHomology.lean 3 declarations
RationalBicomplex.lean 5 declarations
RationalBicomplexComparison.lean 8 declarations
RationalBicomplexHomology.lean 5 declarations
RationalCoefficientDimensionBound.lean 3 declarations
RationalCoefficientHomology.lean 3 declarations
RationalExteriorHomology.lean 12 declarations
RationalFiniteIndexHomology.lean 5 declarations
RationalFiniteResolution.lean 15 declarations
RationalGroupHomology.lean 2 declarations
RationalHomologyDimension.lean 3 declarations
RationalNilpotentHomologyVanishing.lean 7 declarations
RationalNormalExtensionHomology.lean 3 declarations
RationalRankOneHomology.lean 2 declarations
RationalRepresentationFiniteness.lean 3 declarations
RationalRootCoreHomology.lean 6 declarations
RationalTensorHomology.lean 3 declarations
RationalZeroCoefficientHomology.lean 5 declarations
ReducedCohomologyDescent.lean 1 declarations
ReducedCohomologyInput.lean 2 declarations
RegularDualCohomology.lean 1 declarations
RegularProjectiveEvaluation.lean 2 declarations
RepCochainMaps.lean 10 declarations
RepresentationHomologyAction.lean 3 declarations
ResolutionCoefficientSequence.lean 2 declarations
ResolutionHomologyNaturality.lean 4 declarations
RestrictedRegularCohomology.lean 4 declarations
ScalarExtendedRepresentationFiniteness.lean 3 declarations
ScalarHigherHomologyExterior.lean 7 declarations
SequenceVanishingRate.lean 1 declarations
SequentialCohomologyKernel.lean 4 declarations
SequentialCohomologySurjectivity.lean 2 declarations
SequentialProjectiveTelescope.lean 16 declarations
SequentialResolutionVanishing.lean 7 declarations
ShiftedCohomologyDimensionShift.lean 13 declarations
ShiftedCompleteCohomologyAdditive.lean 3 declarations
ShiftedCompleteCohomologyVanishing.lean 5 declarations
ShiftedCompletedCohomology.lean 13 declarations
SmallCoefficientCompletedUnit.lean 7 declarations
SmallCoefficientRing.lean 22 declarations
SolvablePoincareFiniteness.lean 3 declarations
SplitProjectiveColimit.lean 4 declarations
StableResolutionIdentity.lean 11 declarations
StableResolutionLimit.lean 8 declarations
StableSyzygyMap.lean 12 declarations
SubgroupBarResolution.lean 7 declarations
SubgroupInductionDimension.lean 1 declarations
SubgroupResolution.lean 3 declarations
SubgroupTopHomologyDegree.lean 1 declarations
SubsingletonGroupProjective.lean 3 declarations
TensorProjectiveTower.lean 3 declarations
TopHomologyCharacter.lean 2 declarations
TopHomologyKernel.lean 1 declarations
TopHomologyKernelNaturality.lean 2 declarations
TopHomologyNaturality.lean 4 declarations
TrivialGroupDuality.lean 2 declarations
TwistedBilateralCohomology.lean 7 declarations
UnitaryReducedVanishing.lean 3 declarations
VirtualPolycyclicDuality.lean 2 declarations
VirtuallyMetabelianFiniteness.lean 2 declarations