OAI/Analysis/BoundedHochschild/CochainLimitDifferential.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Weak-star limits and the Hochschild differential

Separate weak-star continuity of multiplication, obtained from the predual, lets the bounded Hochschild differential pass through pointwise weak-star limits. No additional normality assumption on the cochains is required.

  1. theorem OAI.BoundedHochschild.predual_tendsto_differential_of_predual line 23

    Source documentation

    The differential preserves pointwise convergence against the predual.

    theorem predual_tendsto_differential_of_predual
    {n : ℕ} {F : I → Cochain M n} {G : Cochain M n} {l : Filter I}
    (h : ∀ x, PredualTendsto e (fun i => F i x) l (G x))
    (x : Fin (n + 1) → M) :
    PredualTendsto e (fun i => differentialValue (F i) x) l (differentialValue G x) := by
…

    Mentions: OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.PredualTendsto, OAI.BoundedHochschild.differentialValue