OAI/Algebra/Finitistic/Localization/
680 declarations, 0 contain sorry, 0 declared as axioms; 79 files
Files
- AdditiveSplitImage.lean 7 declarations
- AmbientQuotientEvaluation.lean 13 declarations
- BoundedDerivedEmbedding.lean 7 declarations
- BoundedHomotopy.lean 12 declarations
- BoundedQuotientEvaluation.lean 17 declarations
- BoundedQuotientGenerators.lean 13 declarations
- BoundedRepresentatives.lean 5 declarations
- ChainRepresentatives.lean 2 declarations
- CompletedCornerEvaluation.lean 9 declarations
- CompletedDerivedEvaluation.lean 10 declarations
- CompletedImageEvaluation.lean 9 declarations
- CompletedOddDoubleEvaluation.lean 3 declarations
- CompletedShiftEvaluation.lean 3 declarations
- CompletedShiftedCornerEvaluation.lean 1 declarations
- ConcreteChainRepresentatives.lean 3 declarations
- ConcreteFixedDiagram.lean 1 declarations
- ConcreteQuadraticDiagram.lean 1 declarations
- ConcreteTensorEvaluation.lean 10 declarations
- DerivedActionCompatibility.lean 5 declarations
- DerivedTruncationCohomology.lean 19 declarations
- DiagramEvaluationSquares.lean 1 declarations
- DiagramLifting.lean 4 declarations
- EvaluationFromAlgebra.lean 4 declarations
- EvaluationLinear.lean 4 declarations
- EvaluationModule.lean 37 declarations
- EvaluationVertexDiagram.lean 6 declarations
- FiniteDerivedEvaluation.lean 15 declarations
- FiniteEvaluationTarget.lean 9 declarations
- FiniteProjectiveHomotopy.lean 13 declarations
- FiniteSumTransport.lean 5 declarations
- FiniteSupportReindex.lean 7 declarations
- FixedDiagram.lean 2 declarations
- FormalSummandAction.lean 18 declarations
- HomotopyEvaluation.lean 3 declarations
- HomotopyVertexEvaluation.lean 9 declarations
- IdempotentImageEvaluation.lean 10 declarations
- IntegerExtensionFunctor.lean 5 declarations
- KaroubiEvaluation.lean 6 declarations
- LocalizedEvaluationStructure.lean 6 declarations
- ModuleActionCompatibility.lean 4 declarations
- NativeArrowBridge.lean 9 declarations
- NativeBoundedDerived.lean 2 declarations
- NativeProjectiveModel.lean 1 declarations
- NativeSingleEvaluation.lean 1 declarations
- NormalizedQuotientAction.lean 6 declarations
- OddDouble.lean 22 declarations
- PresentedActionCompatibility.lean 7 declarations
- PresentedQuotientAction.lean 11 declarations
- ProjectiveComplexes.lean 13 declarations
- QuotientAction.lean 11 declarations
- QuotientActionEvaluation.lean 6 declarations
- QuotientRelations.lean 17 declarations
- SignedCochainShift.lean 3 declarations
- SingleDegreeNaturality.lean 6 declarations
- SourceActionEvaluation.lean 11 declarations
- SourceCornerEvaluation.lean 7 declarations
- SourceEvaluation.lean 34 declarations
- SourceImageEvaluation.lean 18 declarations
- SourceLinear.lean 4 declarations
- SourceModelBridge.lean 14 declarations
- SourceOddDoubleEvaluation.lean 7 declarations
- SourceQuotientAction.lean 20 declarations
- SourceShiftLinear.lean 2 declarations
- SourceVerdier.lean 25 declarations
- SplitComponentExact.lean 3 declarations
- TensorCohomologyDiagram.lean 4 declarations
- TensorEvaluationComparison.lean 4 declarations
- TensorEvaluationFunctor.lean 4 declarations
- ThickEvaluation.lean 10 declarations
- TruncationSplitNaturality.lean 3 declarations
- TruncationStalkNaturality.lean 2 declarations
- TwoConeVerdier.lean 28 declarations
- TwoDegreeExtVanishing.lean 3 declarations
- TwoDegreeFormalityNaturality.lean 7 declarations
- TwoDegreeSplitting.lean 11 declarations
- UnderlyingRepresentatives.lean 7 declarations
- VectorComplexFormality.lean 11 declarations
- VectorIdempotentCompleteness.lean 4 declarations
- VerdierEvaluationExact.lean 4 declarations