feat(topology/algebra): Inf and inducing preserve compatibility with …

…algebraic structure (#11720)

This partly duplicates @mariainesdff 's work on group topologies, but I'm using an unbundled approach which avoids defining a new `X_topology` structure for each interesting X.

src/topology/algebra/group.lean

@@ -844,6 +844,53 @@ def homeomorph.prod_units : homeomorph (α × β)ˣ (αˣ × βˣ) :=
 
 end units
 
+section lattice_ops
+
+variables {ι : Type*} [group G] [group H] {ts : set (topological_space G)}
+  (h : ∀ t ∈ ts, @topological_group G t _) {ts' : ι → topological_space G}
+  (h' : ∀ i, @topological_group G (ts' i) _) {t₁ t₂ : topological_space G}
+  (h₁ : @topological_group G t₁ _) (h₂ : @topological_group G t₂ _)
+  {t : topological_space H} [topological_group H] {F : Type*}
+  [monoid_hom_class F G H] (f : F)
+
+@[to_additive] lemma topological_group_Inf :
+  @topological_group G (Inf ts) _ :=
+{ continuous_inv := continuous_Inf_rng (λ t ht, continuous_Inf_dom ht
+    (@topological_group.continuous_inv G t _ (h t ht))),
+  continuous_mul := @has_continuous_mul.continuous_mul G (Inf ts) _
+    (@has_continuous_mul_Inf _ _ _
+      (λ t ht, @topological_group.to_has_continuous_mul G t _ (h t ht))) }
+
+include h'
+
+@[to_additive] lemma topological_group_infi :
+  @topological_group G (⨅ i, ts' i) _ :=
+by {rw ← Inf_range, exact topological_group_Inf (set.forall_range_iff.mpr h')}
+
+omit h'
+
+include h₁ h₂
+
+@[to_additive] lemma topological_group_inf :
+  @topological_group G (t₁ ⊓ t₂) _ :=
+by {rw inf_eq_infi, refine topological_group_infi (λ b, _), cases b; assumption}
+
+omit h₁ h₂
+
+@[to_additive] lemma topological_group_induced :
+  @topological_group G (t.induced f) _ :=
+{ continuous_inv :=
+    begin
+      letI : topological_space G := t.induced f,
+      refine continuous_induced_rng _,
+      simp_rw [function.comp, map_inv],
+      exact continuous_inv.comp (continuous_induced_dom : continuous f)
+    end,
+  continuous_mul := @has_continuous_mul.continuous_mul G (t.induced f) _
+    (@has_continuous_mul_induced G H _ _ t _ _ _ f) }
+
+end lattice_ops
+
 /-!
 ### Lattice of group topologies
 We define a type class `group_topology α` which endows a group `α` with a topology such that all

src/topology/algebra/module/basic.lean

@@ -127,6 +127,24 @@ end
 
 end
 
+section lattice_ops
+
+variables {ι R M₁ M₂ : Type*} [semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂]
+  [module R M₁] [module R M₂] [u : topological_space R] {t : topological_space M₂}
+  [has_continuous_smul R M₂] (f : M₁ →ₗ[R] M₂)
+
+lemma has_continuous_smul_induced :
+  @has_continuous_smul R M₁ _ u (t.induced f) :=
+{ continuous_smul :=
+    begin
+      letI : topological_space M₁ := t.induced f,
+      refine continuous_induced_rng _,
+      simp_rw [function.comp, f.map_smul],
+      refine continuous_fst.smul (continuous_induced_dom.comp continuous_snd)
+    end }
+
+end lattice_ops
+
 namespace submodule
 
 variables {α β : Type*} [topological_space β]

src/topology/algebra/monoid.lean

@@ -492,3 +492,46 @@ instance additive.has_continuous_add {M} [h : topological_space M] [has_mul M]
 instance multiplicative.has_continuous_mul {M} [h : topological_space M] [has_add M]
   [has_continuous_add M] : @has_continuous_mul (multiplicative M) h _ :=
 { continuous_mul := @continuous_add M _ _ _ }
+
+section lattice_ops
+
+variables [has_mul M] [has_mul N] {ts : set (topological_space M)}
+  (h : Π t ∈ ts, @has_continuous_mul M t _) {ts' : ι → topological_space M}
+  (h' : Π i, @has_continuous_mul M (ts' i) _) {t₁ t₂ : topological_space M}
+  (h₁ : @has_continuous_mul M t₁ _) (h₂ : @has_continuous_mul M t₂ _)
+  {t : topological_space N} [has_continuous_mul N] {F : Type*}
+  [mul_hom_class F M N] (f : F)
+
+@[to_additive] lemma has_continuous_mul_Inf :
+  @has_continuous_mul M (Inf ts) _ :=
+{ continuous_mul := continuous_Inf_rng (λ t ht, continuous_Inf_dom₂ ht ht
+  (@has_continuous_mul.continuous_mul M t _ (h t ht))) }
+
+include h'
+
+@[to_additive] lemma has_continuous_mul_infi :
+  @has_continuous_mul M (⨅ i, ts' i) _ :=
+by {rw ← Inf_range, exact has_continuous_mul_Inf (set.forall_range_iff.mpr h')}
+
+omit h'
+
+include h₁ h₂
+
+@[to_additive] lemma has_continuous_mul_inf :
+  @has_continuous_mul M (t₁ ⊓ t₂) _ :=
+by {rw inf_eq_infi, refine has_continuous_mul_infi (λ b, _), cases b; assumption}
+
+omit h₁ h₂
+
+@[to_additive] lemma has_continuous_mul_induced :
+  @has_continuous_mul M (t.induced f) _ :=
+{ continuous_mul :=
+    begin
+      letI : topological_space M := t.induced f,
+      refine continuous_induced_rng _,
+      simp_rw [function.comp, map_mul],
+      change continuous ((λ p : N × N, p.1 * p.2) ∘ (prod.map f f)),
+      exact continuous_mul.comp (continuous_induced_dom.prod_map continuous_induced_dom),
+    end }
+
+end lattice_ops

src/topology/algebra/mul_action.lean

@@ -322,3 +322,42 @@ instance {ι : Type*} {γ : ι → Type*}
 ⟨continuous_pi $ λ i,
   (continuous_fst.smul continuous_snd).comp $
     continuous_fst.prod_mk ((continuous_apply i).comp continuous_snd)⟩
+
+section lattice_ops
+
+variables {ι : Type*} [has_scalar M β]
+  {ts : set (topological_space β)} (h : Π t ∈ ts, @has_continuous_smul M β _ _ t)
+  {ts' : ι → topological_space β} (h' : Π i, @has_continuous_smul M β _ _ (ts' i))
+  {t₁ t₂ : topological_space β} [h₁ : @has_continuous_smul M β _ _ t₁]
+  [h₂ : @has_continuous_smul M β _ _ t₂]
+
+include h
+
+@[to_additive] lemma has_continuous_smul_Inf :
+  @has_continuous_smul M β _ _ (Inf ts) :=
+{ continuous_smul :=
+  begin
+    rw ← @Inf_singleton _ _ ‹topological_space M›,
+    exact continuous_Inf_rng (λ t ht, continuous_Inf_dom₂ (eq.refl _) ht
+      (@has_continuous_smul.continuous_smul _ _ _ _ t (h t ht)))
+  end }
+
+omit h
+
+include h'
+
+@[to_additive] lemma has_continuous_smul_infi :
+  @has_continuous_smul M β _ _ (⨅ i, ts' i) :=
+by {rw ← Inf_range, exact has_continuous_smul_Inf (set.forall_range_iff.mpr h')}
+
+omit h'
+
+include h₁ h₂
+
+@[to_additive] lemma has_continuous_smul_inf :
+  @has_continuous_smul M β _ _ (t₁ ⊓ t₂) :=
+by {rw inf_eq_infi, refine has_continuous_smul_infi (λ b, _), cases b; assumption}
+
+omit h₁ h₂
+
+end lattice_ops