feat: algebraic versions of LocallyConstant.comap (#6396)

We give algebraic versions of `LocallyConstant.comap` given the relevant algebraic structure on the target.

Mathlib/Topology/LocallyConstant/Algebra.lean

@@ -291,4 +291,49 @@ theorem coe_algebraMap (r : R) : ⇑(algebraMap R (LocallyConstant X Y) r) = alg
 
 end Algebra
 
+section Comap
+
+variable [TopologicalSpace Y]
+
+/-- `LocallyConstant.comap` is a `MonoidHom`. -/
+@[to_additive "`LocallyConstant.comap` is an `AddMonoidHom`."]
+noncomputable
+def comapMonoidHom [MulOneClass Z] (f : X → Y) (hf : Continuous f) :
+    LocallyConstant Y Z →* LocallyConstant X Z where
+  toFun := comap f
+  map_one' := by
+    ext x
+    simp only [hf, coe_comap, coe_one, Function.comp_apply, Pi.one_apply]
+  map_mul' r s := by
+    ext x
+    simp only [hf, coe_comap, coe_mul, Function.comp_apply, Pi.mul_apply]
+
+/-- `LocallyConstant.comap` is a linear map. -/
+noncomputable
+def comapₗ {R : Type _} [Semiring R] [AddCommMonoid Z] [Module R Z] (f : X → Y)
+    (hf : Continuous f) : LocallyConstant Y Z →ₗ[R] LocallyConstant X Z where
+  toFun := comap f
+  map_add' := (comapAddMonoidHom f hf).map_add'
+  map_smul' r s := by
+    ext x
+    simp only [hf, coe_comap, coe_smul, Function.comp_apply, Pi.smul_apply, RingHom.id_apply]
+
+lemma ker_comapₗ {R : Type _} [Semiring R] [AddCommMonoid Z] [Module R Z] (f : X → Y)
+    (hf : Continuous f) (hfs : Function.Surjective f) :
+    LinearMap.ker (comapₗ f hf : LocallyConstant Y Z →ₗ[R] LocallyConstant X Z) = ⊥ :=
+  LinearMap.ker_eq_bot_of_injective <| comap_injective _ hf hfs
+
+/-- `LocallyConstant.congrLeft` is a linear equivalence. -/
+noncomputable
+def congrLeftₗ {R : Type _} [Semiring R] [AddCommMonoid Z] [Module R Z] (e : X ≃ₜ Y) :
+    LocallyConstant X Z ≃ₗ[R] LocallyConstant Y Z where
+  toFun := (congrLeft e).toFun
+  map_smul' := (comapₗ _ e.continuous_invFun).map_smul'
+  map_add' := (comapAddMonoidHom _ e.continuous_invFun).map_add'
+  invFun := (congrLeft e).invFun
+  left_inv := (congrLeft e).left_inv
+  right_inv := (congrLeft e).right_inv
+
+end Comap
+
 end LocallyConstant

Mathlib/Topology/LocallyConstant/Basic.lean

@@ -477,13 +477,17 @@ noncomputable def comap (f : X → Y) : LocallyConstant Y Z → LocallyConstant
 
 @[simp]
 theorem coe_comap (f : X → Y) (g : LocallyConstant Y Z) (hf : Continuous f) :
-    ⇑(comap f g) = g ∘ f := by
+    (comap f g) = g ∘ f := by
   rw [comap, dif_pos hf]
   rfl
 #align locally_constant.coe_comap LocallyConstant.coe_comap
 
+theorem coe_comap_apply (f : X → Y) (g : LocallyConstant Y Z) (hf : Continuous f) (x : X) :
+    comap f g x = g (f x) := by
+  simp only [hf, coe_comap, Function.comp_apply]
+
 @[simp]
-theorem comap_id : @comap X X Z _ _ id = id := by
+theorem comap_id : comap (@id X) = @id (LocallyConstant X Z) := by
   ext
   simp only [continuous_id, id.def, Function.comp.right_id, coe_comap]
 #align locally_constant.comap_id LocallyConstant.comap_id
@@ -495,15 +499,28 @@ theorem comap_comp [TopologicalSpace Z] (f : X → Y) (g : Y → Z) (hf : Contin
   simp only [hf, hg, hg.comp hf, coe_comap]; rfl
 #align locally_constant.comap_comp LocallyConstant.comap_comp
 
+theorem comap_comap [TopologicalSpace Z] (f : X → Y) (g : Y → Z)
+    (hf : Continuous f) (hg : Continuous g) (x : LocallyConstant Z α) :
+    comap f (comap g x) = comap (g ∘ f) x := by
+  rw [← comap_comp f g hf hg]; rfl
+
 theorem comap_const (f : X → Y) (y : Y) (h : ∀ x, f x = y) :
-    (comap f : LocallyConstant Y Z → LocallyConstant X Z) = fun g =>
-      ⟨fun _ => g y, IsLocallyConstant.const _⟩ := by
+    (comap f : LocallyConstant Y Z → LocallyConstant X Z) = fun g => const X (g y) := by
   ext; rw [coe_comap]
-  · simp only [h, coe_mk, Function.comp_apply]
+  · simp only [Function.comp_apply, h, coe_const, Function.const_apply]
   · rw [show f = fun _ => y by ext; apply h]
     exact continuous_const
 #align locally_constant.comap_const LocallyConstant.comap_const
 
+lemma comap_injective (f : X → Y) (hf: Continuous f) (hfs : f.Surjective) :
+    (comap (Z := Z) f).Injective := by
+  intro a b h
+  rw [LocallyConstant.ext_iff] at h
+  ext y
+  obtain ⟨x, hx⟩ := hfs y
+  specialize h x
+  rwa [coe_comap_apply _ _ hf, coe_comap_apply _ _ hf, hx] at h
+
 end Comap
 
 section Desc
@@ -569,6 +586,25 @@ theorem mulIndicator_of_not_mem (hU : IsClopen U) (h : a ∉ U) : f.mulIndicator
 
 end Indicator
 
+section Equiv
+
+/-- The equivalence between `LocallyConstant X Z` and `LocallyConstant Y Z` given a
+    homeomorphism `X ≃ₜ Y` -/
+noncomputable
+def congrLeft [TopologicalSpace Y] (e : X ≃ₜ Y) : LocallyConstant X Z ≃ LocallyConstant Y Z where
+  toFun := comap e.invFun
+  invFun := comap e.toFun
+  left_inv := by
+    intro x
+    rw [comap_comap _ _ e.continuous_toFun e.continuous_invFun x]
+    simp
+  right_inv := by
+    intro x
+    rw [comap_comap _ _ e.continuous_invFun e.continuous_toFun]
+    simp
+
+end Equiv
+
 section Piecewise
 
 /-- Given two closed sets covering a topological space, and locally constant maps on these two sets,