Short exact sequence for ℒ → ℳ

[jcommelin]

• Construct the set-theoretic maps φ : ℒ → ℒ and θ : ℒ → ℳ and show that the first is injective and its image coincides with the kernel of the second.
• Upgrade φ to a morphism Φ of compact-Hausdorffly-filtered-pseudonormed abelian groups.
• Upgrade θ to a morphism Θ of compact-Hausdorffly-filtered-pseudonormed abelian groups.
• Prove that they give rise to an exact sequence of compact-Hausdorffly-filtered-pseudonormed abelian groups.
• Establish the bounds so that the above exact sequence gives rise to an exact sequence of condensed abelian groups as in Proposition 2.5.5 of the Blueprint.