feat(category_theory/Fintype): some lemmas and Fintype_to_Profinite. (

#7491)

Adding some lemmas for morphisms on `Fintype` as functions, as well as `Fintype_to_Profinite`.
Part of the LTE.



Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>

src/category_theory/Fintype.lean

@@ -45,6 +45,16 @@ def incl : Fintype ⥤ Type* := induced_functor _
 
 instance : concrete_category Fintype := ⟨incl⟩
 
+@[simp] lemma coe_id {A : Fintype} : (𝟙 A : A → A) = id := rfl
+
+@[simp] lemma coe_comp {A B C : Fintype} (f : A ⟶ B) (g : B ⟶ C) :
+  (f ≫ g : A → C) = g ∘ f := rfl
+
+lemma id_apply {A : Fintype} (a : A) : (𝟙 A : A → A) a = a := rfl
+
+lemma comp_apply {A B C : Fintype} (f : A ⟶ B) (g : B ⟶ C) (a : A) :
+  (f ≫ g) a = g (f a) := rfl
+
 /--
 The "standard" skeleton for `Fintype`. This is the full subcategory of `Fintype` spanned by objects
 of the form `fin n` for `n : ℕ`. We parameterize the objects of `Fintype.skeleton` directly as `ℕ`,

src/topology/category/Profinite.lean

@@ -9,6 +9,7 @@ import topology.connected
 import topology.subset_properties
 import category_theory.adjunction.reflective
 import category_theory.monad.limits
+import category_theory.Fintype
 
 /-!
 # The category of Profinite Types
@@ -49,7 +50,14 @@ structure Profinite :=
 
 namespace Profinite
 
-instance : inhabited Profinite := ⟨{to_Top := { α := pempty }}⟩
+/--
+Construct a term of `Profinite` from a type endowed with the structure of a
+compact, Hausdorff and totally disconnected topological space.
+-/
+def of (X : Type*) [topological_space X] [compact_space X] [t2_space X]
+  [totally_disconnected_space X] : Profinite := ⟨⟨X⟩⟩
+
+instance : inhabited Profinite := ⟨Profinite.of pempty⟩
 
 instance category : category Profinite := induced_category.category to_Top
 instance concrete_category : concrete_category Profinite := induced_category.concrete_category _
@@ -129,6 +137,24 @@ adjunction.left_adjoint_of_equiv Profinite.to_CompHaus_equivalence (λ _ _ _ _ _
 lemma CompHaus.to_Profinite_obj' (X : CompHaus) :
   ↥(CompHaus.to_Profinite.obj X) = connected_components X.to_Top.α := rfl
 
+ /-- Finite types are given the discrete topology. -/
+def Fintype.discrete_topology (A : Fintype) : topological_space A := ⊥
+
+section discrete_topology
+
+local attribute [instance] Fintype.discrete_topology
+
+/--
+The natural functor from `Fintype` to `Profinite`, endowing a finite type with the
+discrete topology.
+-/
+@[simps]
+def Fintype.to_Profinite : Fintype ⥤ Profinite :=
+{ obj := λ A, Profinite.of A,
+  map := λ _ _ f, ⟨f⟩ }
+
+end discrete_topology
+
 end Profinite
 
 namespace Profinite