adj — Mathlib

Lean4
/-- The completion functor is left adjoint to the forgetful functor. -/
noncomputable def adj : completionFunctor ⊣ forget₂ CpltSepUniformSpace UniformSpaceCat :=
  Adjunction.mkOfHomEquiv
    { homEquiv := fun X Y =>
        { toFun := fun f => completionHom X ≫ f
          invFun := fun f => extensionHom f
          left_inv := fun f => by dsimp; rw [extension_comp_coe]
          right_inv := fun f => by
            ext x
            rcases f with ⟨⟨_, _⟩⟩
            exact @Completion.extension_coe _ _ _ _ _ (CpltSepUniformSpace.t0Space _) ‹_› _ }
      homEquiv_naturality_left_symm := fun {X' X Y} f g => by
        ext x
        dsimp [-Function.comp_apply]
        erw [Completion.extension_map (γ := Y) g.hom.2 f.hom.2]
        rfl }
Похожие утверждения