OAI/Topology/CoarseAssembly.lean
0 declarations, 0 contain sorry, 0 declared as axioms
A bounded-geometry counterexample to coarse Novikov
The concrete graph union has an infinite-order assembly-kernel class, and its constructed analytic assembly map fails to be injective both integrally and rationally.
This file declares nothing itself. It gathers the 175 imports below, so a file that imports it gets all of them.
Imports
- OAI.Topology.CoarseAssembly.FiberedPersistence
- OAI.Topology.CoarseAssembly.HomotopyFilling
- OAI.Topology.CoarseAssembly.LatticeHat
- OAI.Topology.CoarseAssembly.FilledDisc
- OAI.Topology.CoarseAssembly.FilledEdges
- OAI.Topology.CoarseAssembly.FilledWalks
- OAI.Topology.CoarseAssembly.CompactFamilyMap
- OAI.Topology.CoarseAssembly.FamilyFilling
- OAI.Topology.CoarseAssembly.RipsProperEmbedding
- OAI.Topology.CoarseAssembly.RoeInclusion
- OAI.Topology.CoarseAssembly.BoundaryGeometry
- OAI.Topology.CoarseAssembly.BoundaryWalks
- OAI.Topology.CoarseAssembly.BoundaryComponents
- OAI.Topology.CoarseAssembly.HexagonSides
- OAI.Topology.CoarseAssembly.RipsMapCalculus
- OAI.Topology.CoarseAssembly.RipsReindex
- OAI.Topology.CoarseAssembly.ConcretePersistence
- OAI.Topology.CoarseAssembly.BoundaryLoopMaps
- OAI.Topology.CoarseAssembly.BoundaryAssemblyMaps
- OAI.Topology.CoarseAssembly.BoundaryConclusion
- OAI.Topology.CoarseAssembly.PublishedInputReduction
- OAI.Topology.CoarseAssembly.CycleCompactPerturbation
- OAI.Topology.CoarseAssembly.UnitalCycleNormalization
- OAI.Topology.CoarseAssembly.FiniteCycle
- OAI.Topology.CoarseAssembly.FredholmSquare
- OAI.Topology.CoarseAssembly.UnitalCycleInvertible
- OAI.Topology.CoarseAssembly.CompactFunctionalCalculus
- OAI.Topology.CoarseAssembly.RipsEmbedding
- OAI.Topology.CoarseAssembly.ClopenRestriction
- OAI.Topology.CoarseAssembly.ClopenNaturality
- OAI.Topology.CoarseAssembly.CountableAdditivity
- OAI.Topology.CoarseAssembly.SeparatedRips
- OAI.Topology.CoarseAssembly.RipsCompactSupport
- OAI.Topology.CoarseAssembly.RipsFamilyMap
- OAI.Topology.CoarseAssembly.RipsFamilyRestriction
- OAI.Topology.CoarseAssembly.RipsPathCoarsening
- OAI.Topology.CoarseAssembly.CocycleCircleMap
- OAI.Topology.CoarseAssembly.RipsPaths
- OAI.Topology.CoarseAssembly.CocyclePathLifting
- OAI.Topology.CoarseAssembly.FiniteRips
- OAI.Topology.CoarseAssembly.RipsWindingTest
- OAI.Topology.CoarseAssembly.LoopCircle
- OAI.Topology.CoarseAssembly.CirclePairing
- OAI.Topology.CoarseAssembly.FiniteWindingIndex
- OAI.Topology.CoarseAssembly.InclusionModule
- OAI.Topology.CoarseAssembly.BoundaryEmbedding
- OAI.Topology.CoarseAssembly.SeparatedUnion
- OAI.Topology.CoarseAssembly.GraphMetric
- OAI.Topology.CoarseAssembly.SeparatedGeometry
- OAI.Topology.CoarseAssembly.ConcreteSpaces
- OAI.Topology.CoarseAssembly.ConcreteTransferMaps
- OAI.Topology.CoarseAssembly.ConcreteTransfer
- OAI.Topology.CoarseAssembly.Averaging
- OAI.Topology.CoarseAssembly.ProjectionBlocks
- OAI.Topology.CoarseAssembly.SpatialAveraging
- OAI.Topology.CoarseAssembly.AveragingPropagation
- OAI.Topology.CoarseAssembly.KazhdanInput
- OAI.Topology.CoarseAssembly.TensorFibers
- OAI.Topology.CoarseAssembly.TransferCriterion
- OAI.Topology.CoarseAssembly.FiniteFiberMaps
- OAI.Topology.CoarseAssembly.CongruenceSurjective
- OAI.Topology.CoarseAssembly.CongruenceEdgeOperators
- OAI.Topology.CoarseAssembly.GraphFiberOperators
- OAI.Topology.CoarseAssembly.PathFiberOperators
- OAI.Topology.CoarseAssembly.DiscConnected
- OAI.Topology.CoarseAssembly.FiberConnected
- OAI.Topology.CoarseAssembly.FiberDegree
- OAI.Topology.CoarseAssembly.AnalyticKHomology
- OAI.Topology.CoarseAssembly.Assembly
- OAI.Topology.CoarseAssembly.BoundaryIndex
- OAI.Topology.CoarseAssembly.BlockOperators
- OAI.Topology.CoarseAssembly.BoundedGeometry
- OAI.Topology.CoarseAssembly.ChosenHolonomy
- OAI.Topology.CoarseAssembly.CongruenceQuotients
- OAI.Topology.CoarseAssembly.CongruenceMaps
- OAI.Topology.CoarseAssembly.CongruenceFibers
- OAI.Topology.CoarseAssembly.Conjugation
- OAI.Topology.CoarseAssembly.ControlledMatrices
- OAI.Topology.CoarseAssembly.FiniteWords
- OAI.Topology.CoarseAssembly.FiberedGraph
- OAI.Topology.CoarseAssembly.FiberConstants
- OAI.Topology.CoarseAssembly.FiberEmbedding
- OAI.Topology.CoarseAssembly.FredholmModule
- OAI.Topology.CoarseAssembly.Holonomy
- OAI.Topology.CoarseAssembly.HilbertSum
- OAI.Topology.CoarseAssembly.Lattice
- OAI.Topology.CoarseAssembly.LatticeCharge
- OAI.Topology.CoarseAssembly.LocallyFinite
- OAI.Topology.CoarseAssembly.NonUnitalK1
- OAI.Topology.CoarseAssembly.Persistence
- OAI.Topology.CoarseAssembly.RipsRealization
- OAI.Topology.CoarseAssembly.Roe
- OAI.Topology.CoarseAssembly.RoeCalculus
- OAI.Topology.CoarseAssembly.RoeTransfer
- OAI.Topology.CoarseAssembly.RoeRows
- OAI.Topology.CoarseAssembly.Sandwich
- OAI.Topology.CoarseAssembly.ShortLoops
- OAI.Topology.CoarseAssembly.SpatialBlocks
- OAI.Topology.CoarseAssembly.TopologicalK1
- OAI.Topology.CoarseAssembly.TraceObstruction
- OAI.Topology.CoarseAssembly.TraceSeparation
- OAI.Topology.CoarseAssembly.TransferLift
- OAI.Topology.CoarseAssembly.RealNormalization
- OAI.Topology.CoarseAssembly.InvolutiveNormalization
- OAI.Topology.CoarseAssembly.ScalarCycleNormalization
- OAI.Topology.CoarseAssembly.LocalCompactPerturbation
- OAI.Topology.CoarseAssembly.ScalarCutDown
- OAI.Topology.CoarseAssembly.SupportedNormalization
- OAI.Topology.CoarseAssembly.PointCoefficient
- OAI.Topology.CoarseAssembly.FredholmParametrix
- OAI.Topology.CoarseAssembly.ToeplitzCompression
- OAI.Topology.CoarseAssembly.CycleIndex
- OAI.Topology.CoarseAssembly.RepresentedCutDown
- OAI.Topology.CoarseAssembly.RepresentedNormalization
- OAI.Topology.CoarseAssembly.RepresentedIndex
- OAI.Topology.CoarseAssembly.CompactIndex
- OAI.Topology.CoarseAssembly.OperatorNormalization
- OAI.Topology.CoarseAssembly.EssentialToeplitz
- OAI.Topology.CoarseAssembly.ExplicitCutDown
- OAI.Topology.CoarseAssembly.RawCycleIndex
- OAI.Topology.CoarseAssembly.DegenerateCutDown
- OAI.Topology.CoarseAssembly.UnitaryIndex
- OAI.Topology.CoarseAssembly.CompactIndexPairing
- OAI.Topology.CoarseAssembly.CircleInputReduction
- OAI.Topology.CoarseAssembly.CircleCoefficient
- OAI.Topology.CoarseAssembly.ExplicitCircleFamily
- OAI.Topology.CoarseAssembly.ExplicitBoundaryConclusion
- OAI.Topology.CoarseAssembly.StructureQuotient
- OAI.Topology.CoarseAssembly.ControlledBoundaryHomotopy
- OAI.Topology.CoarseAssembly.CayleyNaturality
- OAI.Topology.CoarseAssembly.RipsPartition
- OAI.Topology.CoarseAssembly.PartitionIsometry
- OAI.Topology.CoarseAssembly.RipsBoundaryRepresentative
- OAI.Topology.CoarseAssembly.AmpleRipsFamily
- OAI.Topology.CoarseAssembly.MultiplierBoundaryHomotopy
- OAI.Topology.CoarseAssembly.RelativeNaturality
- OAI.Topology.CoarseAssembly.SeparatedFamilyHomotopy
- OAI.Topology.CoarseAssembly.SeparatedFamilyPerturbation
- OAI.Topology.CoarseAssembly.SpatialBoundaryNaturality
- OAI.Topology.CoarseAssembly.CoefficientRoeHom
- OAI.Topology.CoarseAssembly.PartitionInclusion
- OAI.Topology.CoarseAssembly.CoefficientInclusion
- OAI.Topology.CoarseAssembly.ExplicitBoundaryRepresentative
- OAI.Topology.CoarseAssembly.NormalizedRipsFamily
- OAI.Topology.CoarseAssembly.RipsBoundaryDegeneracy
- OAI.Topology.CoarseAssembly.RipsFamilyCompactPerturbation
- OAI.Topology.CoarseAssembly.RipsScaleCompatibility
- OAI.Topology.CoarseAssembly.MultiplierUnitaryHomotopy
- OAI.Topology.CoarseAssembly.RelativeTwoDiagonal
- OAI.Topology.CoarseAssembly.IsometryDilation
- OAI.Topology.CoarseAssembly.RelativePartialIsometry
- OAI.Topology.CoarseAssembly.MultiplierIsometryInvariance
- OAI.Topology.CoarseAssembly.RipsEmbeddingIndependence
- OAI.Topology.CoarseAssembly.PointwiseEmbeddingTransition
- OAI.Topology.CoarseAssembly.RipsUnitaryFamily
- OAI.Topology.CoarseAssembly.OrthogonalSumBoundary
- OAI.Topology.CoarseAssembly.RipsDirectSumBoundary
- OAI.Topology.CoarseAssembly.SeparatedFamilyNearby
- OAI.Topology.CoarseAssembly.ControlledCoarseAssembly
- OAI.Topology.CoarseAssembly.RipsFiniteHomotopy
- OAI.Topology.CoarseAssembly.RipsFixedRepresentationHomotopy
- OAI.Topology.CoarseAssembly.RipsUnrestrictedHomotopy
- OAI.Topology.CoarseAssembly.RegularizedRipsFamily
- OAI.Topology.CoarseAssembly.BoundedTransformNaturality
- OAI.Topology.CoarseAssembly.SeparatedRipsIndex
- OAI.Topology.CoarseAssembly.RipsFiniteTail
- OAI.Topology.CoarseAssembly.RegularizedCoarsening
- OAI.Topology.CoarseAssembly.LateRipsCoarsening
- OAI.Topology.CoarseAssembly.SeparatedCoarseAssembly
- OAI.Topology.CoarseAssembly.SeparatedIndexNaturality
- OAI.Topology.CoarseAssembly.IndexFamilyTransport
- OAI.Topology.CoarseAssembly.ConstructedConclusion
- OAI.Topology.CoarseAssembly.AveragingEnergy
- OAI.Topology.CoarseAssembly.RegularConstants
- OAI.Topology.CoarseAssembly.UnconditionalConclusion