feat(Profinite): the functors from FintypeCat are fully faithful (#…

…12139) (both to `LightProfinite` and `Profinite`)
leanprover-community · Apr 15, 2024 · 5d49276 · 5d49276
1 parent d48d30a
commit 5d49276
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git a/Mathlib/Topology/Category/LightProfinite/Basic.lean b/Mathlib/Topology/Category/LightProfinite/Basic.lean
@@ -98,6 +98,13 @@ def fintypeCatToLightProfinite : FintypeCat ⥤ LightProfinite.{u} where
   obj X := X.toLightProfinite
   map f := FintypeCat.toProfinite.map f
 
+instance : fintypeCatToLightProfinite.Faithful where
+  map_injective h := funext fun _ ↦ (DFunLike.ext_iff.mp h) _
+
+instance : fintypeCatToLightProfinite.Full where
+  preimage f := fun x ↦ f x
+  witness _ := rfl
+
 end LightProfinite
 
 noncomputable section EssentiallySmall

diff --git a/Mathlib/Topology/Category/Profinite/Basic.lean b/Mathlib/Topology/Category/Profinite/Basic.lean
@@ -236,6 +236,13 @@ def FintypeCat.toProfinite : FintypeCat ⥤ Profinite where
   map f := ⟨f, by continuity⟩
 #align Fintype.to_Profinite FintypeCat.toProfinite
 
+instance : FintypeCat.toProfinite.Faithful where
+  map_injective h := funext fun _ ↦ (DFunLike.ext_iff.mp h) _
+
+instance : FintypeCat.toProfinite.Full where
+  preimage f := fun x ↦ f x
+  witness _ := rfl
+
 end DiscreteTopology
 
 end Profinite