`OAI/Topology/ArtinGroups/Complexes/`

1040 declarations, 0 contain sorry, 0 declared as axioms; 200 files

Files

ActedIndex.lean 15 declarations
ArrowShift.lean 14 declarations
BasedComplexComplex.lean 8 declarations
BlockClosed.lean 14 declarations
BottomScalarCycleInjective.lean 2 declarations
BottomScalarCycleZero.lean 1 declarations
BottomSocleZero.lean 3 declarations
BottomSocleZeroTest.lean 1 declarations
CanonicalLowReflectedHigh.lean 1 declarations
CanonicalWordLow.lean 3 declarations
Capped.lean 8 declarations
CochainSignSubOne.lean 15 declarations
CoconePlacement.lean 8 declarations
CoefficientIncoming.lean 8 declarations
CoefficientSocle.lean 9 declarations
CoefficientSocleRestrictLayer.lean 1 declarations
CoefficientTopDual.lean 13 declarations
CoefficientTopDualRestrict.lean 2 declarations
ColorBoundary.lean 7 declarations
ColorReduction.lean 6 declarations
ColorRestrictionTopZero.lean 1 declarations
ColorSupport.lean 9 declarations
CommuteTwistSwap.lean 3 declarations
ComplexPacketLowerBound.lean 3 declarations
ComplexPacketPreserves.lean 2 declarations
Cone.lean 3 declarations
Cone2.lean 6 declarations
ConeMap.lean 8 declarations
ConePlacement.lean 6 declarations
CornerPath.lean 6 declarations
CorrectionBoundary.lean 3 declarations
DiagonalVertex.lean 13 declarations
Differential.lean 6 declarations
DifferentialMulExtendLayer.lean 4 declarations
DownClosed.lean 20 declarations
EmptyTestIndex.lean 6 declarations
EqualColorPair.lean 6 declarations
ExtendLayer.lean 8 declarations
FamilySubobjectMiddleLower.lean 1 declarations
FiniteFamilyLevelSupport.lean 1 declarations
FiniteHomotopySetoid.lean 12 declarations
FiniteSum.lean 4 declarations
FiniteSum2.lean 5 declarations
FrameCappedInjection.lean 1 declarations
FrameModelLayerMiddle.lean 2 declarations
FrameModelNegativeHom.lean 2 declarations
GeneratorArray.lean 7 declarations
GeneratorArray2.lean 8 declarations
GeneratorArrayZeroCap.lean 2 declarations
GeneratorArrayZeroLevel.lean 1 declarations
GeneratorTokenTest.lean 3 declarations
GeneratorVector.lean 8 declarations
GeneratorVectorPos.lean 1 declarations
GeneratorVectorPureLayer.lean 2 declarations
HighConeIndex.lean 7 declarations
HighConeRetainedPure.lean 6 declarations
HighDualCycleZero.lean 2 declarations
HighestLocalGeneratorTest.lean 7 declarations
HomDetector.lean 3 declarations
HomDimension.lean 5 declarations
HomDimension2.lean 4 declarations
HomDimensionDual.lean 7 declarations
HomDimensionRetract.lean 4 declarations
HomDimensionZeroCycles.lean 3 declarations
HomDimensionZeroHom.lean 4 declarations
HomInternalSupport.lean 8 declarations
HomMono.lean 6 declarations
HomOperator.lean 8 declarations
HomPath.lean 9 declarations
HomSpace.lean 15 declarations
HomSpaceDuality.lean 6 declarations
HomSpaceMul.lean 7 declarations
HomSpacePairing.lean 3 declarations
HomStep.lean 7 declarations
HomotopyConeMap.lean 7 declarations
Identity.lean 8 declarations
Initial.lean 6 declarations
InitialHomSpaceNegative.lean 2 declarations
InitialProbeTestUpper.lean 3 declarations
InitialProjective.lean 10 declarations
InverseHomMatrix.lean 7 declarations
InverseMatrix.lean 11 declarations
InverseTwistDifferential.lean 4 declarations
InverseTwistIdentity.lean 8 declarations
InverseTwistIndex.lean 5 declarations
InverseTwistMap.lean 5 declarations
InverseTwistPlacement.lean 11 declarations
InverseWordAction.lean 8 declarations
InverseWordActionAppend.lean 4 declarations
IsolatedIndexCycle.lean 2 declarations
LayerConeEquivalence.lean 1 declarations
LayerSocleDimensionLayer.lean 5 declarations
LayerSocleDimensionSum.lean 2 declarations
LayerTotalHomDimension.lean 2 declarations
LayerVector.lean 5 declarations
LeftMatrix.lean 4 declarations
LevelArrayBelow.lean 1 declarations
LevelArrayComplexMinimal.lean 3 declarations
LevelArrayMinimalApply.lean 6 declarations
LowMatrix.lean 8 declarations
LowerTruncation.lean 4 declarations
LowerTruncationLayerFloor.lean 5 declarations
LowerTruncationSum.lean 2 declarations
MatrixOneMulExtend.lean 3 declarations
Middle.lean 6 declarations
MinimalEmbedding.lean 1 declarations
MinimalGeneratorDualCycle.lean 2 declarations
MinimalModel.lean 8 declarations
MinimalModelEquivalence.lean 7 declarations
NegativeAmplitudeCoreIndex.lean 14 declarations
NegativeConeIndex.lean 5 declarations
NegativeHomTransformReflect.lean 4 declarations
NegativeTwistCapDisjoint.lean 7 declarations
NegativeTwistLoweredGenerator.lean 2 declarations
NegativeTwistModern.lean 12 declarations
NormalizedInverseTwistHomotopy.lean 2 declarations
NormalizedReverseTwistHomotopy.lean 2 declarations
OptionSumEquiv.lean 7 declarations
OutsideCap.lean 7 declarations
PacketConsEquiv.lean 6 declarations
PacketLayerLowerTruncation.lean 3 declarations
PacketPermAction.lean 1 declarations
PacketPermEnumeration.lean 3 declarations
PacketPermExterior.lean 3 declarations
PacketPermPreservesOpen.lean 1 declarations
PacketPermReindex.lean 5 declarations
PacketTwistRaisedGenerator.lean 2 declarations
PacketTwistRaisedGenerator2.lean 3 declarations
PacketTwistTopZero.lean 2 declarations
PlacedProjective.lean 7 declarations
PlacementSignedWeight.lean 10 declarations
PositiveConeIndex.lean 5 declarations
PositiveHomTransform.lean 10 declarations
PositiveTopDivisor.lean 1 declarations
PositiveTwistFiberEquiv.lean 4 declarations
PositiveTwistHomotopy.lean 14 declarations
PositiveTwistLowerBound.lean 4 declarations
PositiveTwistModern.lean 6 declarations
PositiveTwistOtherTest.lean 2 declarations
PositiveTwistOtherTest2.lean 1 declarations
PositiveTwistOtherTest3.lean 1 declarations
PositiveTwistRaisedGenerator.lean 2 declarations
PositiveTwistUnshiftedLayer.lean 1 declarations
PositiveWord.lean 7 declarations
PositiveWordActionAppend.lean 2 declarations
PositiveWordActionOrthogonal.lean 3 declarations
PositiveWordActionTest.lean 2 declarations
PositiveWordLowerBound.lean 3 declarations
ProbeFixedNoDiagonal.lean 1 declarations
ProbeHomDimensionGenerator.lean 1 declarations
ProbeOrbitGeneratorExterior.lean 2 declarations
ProbeOrbitLevelDual.lean 1 declarations
PureCoefficientCohomology.lean 5 declarations
PureHomSpaceHomogeneous.lean 5 declarations
PureLayerSelf.lean 7 declarations
PureSupportedCycles.lean 6 declarations
PureTotalHomEuler.lean 1 declarations
PureUpperBoundariesZero.lean 2 declarations
ReducedAmplitudeTwistLevel.lean 3 declarations
ReducedNegativeAmplitudeTwist.lean 3 declarations
ReducedNoTopDivisor.lean 2 declarations
Refl.lean 8 declarations
Reindex.lean 5 declarations
ReindexConeIsomorphism.lean 2 declarations
ReindexHomOperator.lean 4 declarations
RestrictExtendLayerMul.lean 2 declarations
RestrictLayer.lean 7 declarations
ReverseTwistDifferential.lean 3 declarations
ReverseTwistIndexEquiv.lean 3 declarations
ReverseTwistProjection.lean 9 declarations
ReverseTwistProjectionCommute.lean 4 declarations
ScalarExactNotZero.lean 3 declarations
ScalarKernel.lean 14 declarations
ScalarSupported.lean 6 declarations
ScalarSupportedCochainShift.lean 3 declarations
ScalarSupportedTokenShift.lean 4 declarations
SecondaryLayer.lean 5 declarations
Shift.lean 7 declarations
SubobjectMiddleLowerBound.lean 2 declarations
Subrepresentation.lean 7 declarations
Sum.lean 5 declarations
SumTestEquiv.lean 10 declarations
SumTruncationEquiv.lean 2 declarations
SummandSecondary.lean 3 declarations
SupportedCoefficientCycles.lean 5 declarations
TargetLow.lean 7 declarations
TermwiseSplitInjection.lean 7 declarations
Test.lean 3 declarations
TestComplexVertexDifferential.lean 3 declarations
TestExact.lean 9 declarations
TestUpperBound.lean 8 declarations
TokenShift.lean 9 declarations
TotalHomDimensionReading.lean 1 declarations
TotalVector.lean 12 declarations
TotalVectorLayer.lean 4 declarations
TwistNewTestIndex.lean 5 declarations
UnfoldedCartanSymm.lean 5 declarations
UnfoldedPresentation.lean 4 declarations
UpperBound.lean 7 declarations
WordInverseModel.lean 9 declarations