feat(data/set/basic,order/filter/basic): add semiconj lemmas about im…

…ages and maps (#14970)

This adds `function.commute` and `function.semiconj` lemmas, and replaces all the uses of `_comm` lemmas with the `semiconj` version as it turns out that only this generality is needed.

src/data/finset/basic.lean

@@ -1921,6 +1921,15 @@ lemma map_comm {β'} {f : β ↪ γ} {g : α ↪ β} {f' : α ↪ β'} {g' : β'
   (s.map g).map f = (s.map f').map g' :=
 by simp_rw [map_map, embedding.trans, function.comp, h_comm]
 
+lemma _root_.function.semiconj.finset_map {f : α ↪ β} {ga : α ↪ α} {gb : β ↪ β}
+  (h : function.semiconj f ga gb) :
+  function.semiconj (map f) (map ga) (map gb) :=
+λ s, map_comm h
+
+lemma _root_.function.commute.finset_map {f g : α ↪ α} (h : function.commute f g) :
+  function.commute (map f) (map g) :=
+h.finset_map
+
 @[simp] theorem map_subset_map {s₁ s₂ : finset α} : s₁.map f ⊆ s₂.map f ↔ s₁ ⊆ s₂ :=
 ⟨λ h x xs, (mem_map' _).1 $ h $ (mem_map' f).2 xs,
  λ h, by simp [subset_def, map_subset_map h]⟩
@@ -2095,6 +2104,16 @@ lemma image_comm {β'} [decidable_eq β'] [decidable_eq γ] {f : β → γ} {g :
   (s.image g).image f = (s.image f').image g' :=
 by simp_rw [image_image, comp, h_comm]
 
+lemma _root_.function.semiconj.finset_image [decidable_eq α] {f : α → β} {ga : α → α} {gb : β → β}
+  (h : function.semiconj f ga gb) :
+  function.semiconj (image f) (image ga) (image gb) :=
+λ s, image_comm h
+
+lemma _root_.function.commute.finset_image [decidable_eq α] {f g : α → α}
+  (h : function.commute f g) :
+  function.commute (image f) (image g) :=
+h.finset_image
+
 theorem image_subset_image {s₁ s₂ : finset α} (h : s₁ ⊆ s₂) : s₁.image f ⊆ s₂.image f :=
 by simp only [subset_def, image_val, subset_dedup', dedup_subset',
   multiset.map_subset_map h]

src/data/finset/pointwise.lean

@@ -775,7 +775,7 @@ variables [decidable_eq γ]
 @[to_additive]
 instance smul_comm_class_finset [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :
   smul_comm_class α β (finset γ) :=
-⟨λ _ _ _, image_comm $ smul_comm _ _⟩
+⟨λ _ _, commute.finset_image $ smul_comm _ _⟩
 
 @[to_additive]
 instance smul_comm_class_finset' [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :

src/data/set/basic.lean

@@ -1422,6 +1422,15 @@ lemma image_comm {β'} {f : β → γ} {g : α → β} {f' : α → β'} {g' : 
   (s.image g).image f = (s.image f').image g' :=
 by simp_rw [image_image, h_comm]
 
+lemma _root_.function.semiconj.set_image {f : α → β} {ga : α → α} {gb : β → β}
+  (h : function.semiconj f ga gb) :
+  function.semiconj (image f) (image ga) (image gb) :=
+λ s, image_comm h
+
+lemma _root_.function.commute.set_image {f g : α → α} (h : function.commute f g) :
+  function.commute (image f) (image g) :=
+h.set_image
+
 /-- Image is monotone with respect to `⊆`. See `set.monotone_image` for the statement in
 terms of `≤`. -/
 theorem image_subset {a b : set α} (f : α → β) (h : a ⊆ b) : f '' a ⊆ f '' b :=

src/data/set/pointwise.lean

@@ -164,7 +164,8 @@ by { rw ←image_inv, exact (range_comp _ _).symm }
 open mul_opposite
 
 @[to_additive]
-lemma image_op_inv : op '' s⁻¹ = (op '' s)⁻¹ := by simp_rw [←image_inv, image_comm op_inv]
+lemma image_op_inv : op '' s⁻¹ = (op '' s)⁻¹ :=
+by simp_rw [←image_inv, function.semiconj.set_image op_inv s]
 
 end has_involutive_inv
 end inv
@@ -946,7 +947,7 @@ ext $ λ x, ⟨λ hx, let ⟨p, q, ⟨i, hi⟩, ⟨j, hj⟩, hpq⟩ := set.mem_s
 @[to_additive]
 instance smul_comm_class_set [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :
   smul_comm_class α β (set γ) :=
-⟨λ _ _ _, image_comm $ smul_comm _ _⟩
+⟨λ _ _, commute.set_image $ smul_comm _ _⟩
 
 @[to_additive]
 instance smul_comm_class_set' [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :

src/order/filter/basic.lean

@@ -1702,6 +1702,22 @@ lemma comap_comm (G : filter δ) : comap φ (comap ψ G) = comap θ (comap ρ G)
 by rw [filter.comap_comap, H, ← filter.comap_comap]
 end comm
 
+lemma _root_.function.semiconj.filter_map {f : α → β} {ga : α → α} {gb : β → β}
+  (h : function.semiconj f ga gb) : function.semiconj (map f) (map ga) (map gb) :=
+map_comm h.comp_eq
+
+lemma _root_.commute.filter_map {f g : α → α} (h : function.commute f g) :
+  function.commute (map f) (map g) :=
+h.filter_map
+
+lemma _root_.function.semiconj.filter_comap {f : α → β} {ga : α → α} {gb : β → β}
+  (h : function.semiconj f ga gb) : function.semiconj (comap f) (comap gb) (comap ga) :=
+comap_comm h.comp_eq.symm
+
+lemma _root_.commute.filter_comap {f g : α → α} (h : function.commute f g) :
+  function.commute (comap f) (comap g) :=
+h.filter_comap
+
 @[simp] theorem comap_principal {t : set β} : comap m (𝓟 t) = 𝓟 (m ⁻¹' t) :=
 filter.ext $ λ s,
   ⟨λ ⟨u, (hu : t ⊆ u), (b : preimage m u ⊆ s)⟩, (preimage_mono hu).trans b,

src/order/filter/pointwise.lean

@@ -480,7 +480,7 @@ by simp only [is_unit_iff, group.is_unit, and_true]
 
 include β
 
-@[to_additive] lemma map_inv' : f⁻¹.map m = (f.map m)⁻¹ := map_comm (funext $ map_inv m) _
+@[to_additive] lemma map_inv' : f⁻¹.map m = (f.map m)⁻¹ := semiconj.filter_map (map_inv m) f
 
 @[to_additive] lemma tendsto.inv_inv : tendsto m f₁ f₂ → tendsto m f₁⁻¹ f₂⁻¹ :=
 λ hf, (filter.map_inv' m).trans_le $ filter.inv_le_inv hf

src/topology/algebra/field.lean

@@ -90,15 +90,14 @@ variables [topological_division_ring K]
 
 lemma units_top_group : topological_group Kˣ :=
 { continuous_inv := begin
-     have : (coe : Kˣ → K) ∘ (λ x, x⁻¹ : Kˣ → Kˣ) =
-            (λ x, x⁻¹ : K → K) ∘ (coe : Kˣ → K), from funext units.coe_inv,
-     rw continuous_iff_continuous_at,
-     intros x,
-     rw [continuous_at, nhds_induced, nhds_induced, tendsto_iff_comap, comap_comm this],
-     apply comap_mono,
-     rw [← tendsto_iff_comap, units.coe_inv],
-     exact continuous_at_inv₀ x.ne_zero
-   end ,
+    rw continuous_iff_continuous_at,
+    intros x,
+    rw [continuous_at, nhds_induced, nhds_induced, tendsto_iff_comap,
+      ←function.semiconj.filter_comap units.coe_inv _],
+    apply comap_mono,
+    rw [← tendsto_iff_comap, units.coe_inv],
+    exact continuous_at_inv₀ x.ne_zero
+  end,
   ..topological_ring.top_monoid_units K}
 
 local attribute [instance] units_top_group