From e0ce21862273a48e47abe598035d4d043e3e3ecb Mon Sep 17 00:00:00 2001
From: Jireh Loreaux <loreaujy@gmail.com>
Date: Fri, 14 Oct 2022 10:34:10 +0000
Subject: [PATCH] =?UTF-8?q?feat(analysis/normed=5Fspace/star/gelfand=5Fdua?=
 =?UTF-8?q?lity):=20functoriality=20of=20`character=5Fspace=20=E2=84=82`?=
 =?UTF-8?q?=20(#16835)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This is one of the two contravariant functors involved in Gelfand duality.
---
 .../normed_space/star/gelfand_duality.lean    | 42 +++++++++++++++++++
 1 file changed, 42 insertions(+)

diff --git a/src/analysis/normed_space/star/gelfand_duality.lean b/src/analysis/normed_space/star/gelfand_duality.lean
index 501f3d88a7b3a..ac95ef0534b3d 100644
--- a/src/analysis/normed_space/star/gelfand_duality.lean
+++ b/src/analysis/normed_space/star/gelfand_duality.lean
@@ -24,6 +24,8 @@ and even an equivalence between C⋆-algebras.
 
 * `ideal.to_character_space` : constructs an element of the character space from a maximal ideal in
   a commutative complex Banach algebra
+* `weak_dual.character_space.comp_continuous_map`: The functorial map taking `ψ : A →⋆ₐ[ℂ] B` to a
+  continuous function `character_space ℂ B → character_space ℂ A` given by pre-composition with `ψ`.
 
 ## Main statements
 
@@ -164,3 +166,43 @@ begin
 end
 
 end complex_cstar_algebra
+
+section functoriality
+
+namespace weak_dual
+
+namespace character_space
+
+variables {A B C : Type*}
+variables [normed_ring A] [normed_algebra ℂ A] [complete_space A] [star_ring A]
+variables [normed_ring B] [normed_algebra ℂ B] [complete_space B] [star_ring B]
+variables [normed_ring C] [normed_algebra ℂ C] [complete_space C] [star_ring C]
+
+/-- The functorial map taking `ψ : A →⋆ₐ[ℂ] B` to a continuous function
+`character_space ℂ B → character_space ℂ A` obtained by pre-composition with `ψ`. -/
+@[simps]
+noncomputable def comp_continuous_map (ψ : A →⋆ₐ[ℂ] B) :
+  C(character_space ℂ B, character_space ℂ A) :=
+{ to_fun := λ φ, equiv_alg_hom.symm ((equiv_alg_hom φ).comp (ψ.to_alg_hom)),
+  continuous_to_fun := continuous.subtype_mk (continuous_of_continuous_eval $
+    λ a, map_continuous $ gelfand_transform ℂ B (ψ a)) _ }
+
+variables (A)
+
+/-- `weak_dual.character_space.comp_continuous_map` sends the identity to the identity. -/
+@[simp] lemma comp_continuous_map_id :
+  comp_continuous_map (star_alg_hom.id ℂ A) = continuous_map.id (character_space ℂ A) :=
+continuous_map.ext $ λ a, ext $ λ x, rfl
+
+variables {A}
+
+/-- `weak_dual.character_space.comp_continuous_map` is functorial. -/
+@[simp] lemma comp_continuous_map_comp (ψ₂ : B →⋆ₐ[ℂ] C) (ψ₁ : A →⋆ₐ[ℂ] B) :
+  comp_continuous_map (ψ₂.comp ψ₁) = (comp_continuous_map ψ₁).comp (comp_continuous_map ψ₂) :=
+continuous_map.ext $ λ a, ext $ λ x, rfl
+
+end character_space
+
+end weak_dual
+
+end functoriality