Assembly.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Compatible analytic indices and their coarsening limit

The scale-index homomorphisms and their compatibility are the precise published input from Willett--Yu, Higher Index Theory, §§5.1, 6.7, 7.1--7.2 (with errata 30--31). Their source is the Fredholm-module group of the actual C₀ algebra; their target is the topological K₁ of the actual nonunital algebra. The induced coarse map is constructed here by the universal property of the direct limit. No geometric detection, filling or transfer conclusion is part of this input.

theorem OAI.CoarseAssembly.Analytic.CoarseningMorphism.pushforward_compatible line 30
def OAI.CoarseAssembly.Analytic.CoarseningMorphism.homologyMap line 37
theorem OAI.CoarseAssembly.Analytic.CoarseningMorphism.homologyMap_of line 41
theorem OAI.CoarseAssembly.Analytic.CompatibleIndexFamily.assembly_of line 53

theorem OAI.CoarseAssembly.Analytic.CompatibleIndexFamily.assembly_natural line 58

Source documentation

Scale-level analytic naturality passes to the actual coarsening limit.

theorem assembly_natural (I : CompatibleIndexFamily C A) (J : CompatibleIndexFamily D B)
    (f : CoarseningMorphism C D) (φ : A →⋆ₙₐ[ℂ] B)
    (hnat : ∀ r, (J.atScale r).comp (pushforward (f.atScale r)) =
      (OperatorKTheory.map φ).comp (I.atScale r)) :
    J.assembly.comp f.homologyMap = (OperatorKTheory.map φ).comp I.assembly := by
…

Mentions: OAI.CoarseAssembly.Analytic.CompatibleIndexFamily, OAI.CoarseAssembly.Analytic.CoarseningMorphism, OAI.CoarseAssembly.Analytic.pushforward, OAI.CoarseAssembly.OperatorKTheory.map