refactor(order/filter/pointwise): Cleanup (#12789)

* Reduce typeclass assumptions from `monoid` to `has_mul`
* Turn lemmas into instances
* Use hom classes rather than concrete hom types
* Golf

src/algebra/pointwise.lean

@@ -62,7 +62,7 @@ pointwise subtraction
 
 open function
 
-variables {α β γ : Type*}
+variables {F α β γ : Type*}
 
 /-! ### Sets -/
 
@@ -239,10 +239,6 @@ lemma preimage_mul_left_one' [group α] : (λ b, a⁻¹ * b) ⁻¹' 1 = {a} := b
 @[to_additive]
 lemma preimage_mul_right_one' [group α] : (* b⁻¹) ⁻¹' 1 = {b} := by simp
 
-@[to_additive]
-protected lemma mul_comm [comm_semigroup α] : s * t = t * s :=
-by simp only [← image2_mul, image2_swap _ s, mul_comm]
-
 /-- `set α` is a `mul_one_class` under pointwise operations if `α` is. -/
 @[to_additive /-"`set α` is an `add_zero_class` under pointwise operations if `α` is."-/]
 protected def mul_one_class [mul_one_class α] : mul_one_class (set α) :=
@@ -256,6 +252,12 @@ protected def semigroup [semigroup α] : semigroup (set α) :=
 { mul_assoc := λ _ _ _, image2_assoc mul_assoc,
   ..set.has_mul }
 
+/-- `set α` is a `comm_semigroup` under pointwise operations if `α` is. -/
+@[to_additive "`set α` is an `add_comm_semigroup` under pointwise operations if `α` is."]
+protected def comm_semigroup [comm_semigroup α] : comm_semigroup (set α) :=
+{ mul_comm := λ s t, by simp only [← image2_mul, image2_swap _ s, mul_comm]
+  ..set.semigroup }
+
 /-- `set α` is a `monoid` under pointwise operations if `α` is. -/
 @[to_additive /-"`set α` is an `add_monoid` under pointwise operations if `α` is. "-/]
 protected def monoid [monoid α] : monoid (set α) :=
@@ -265,10 +267,11 @@ protected def monoid [monoid α] : monoid (set α) :=
 /-- `set α` is a `comm_monoid` under pointwise operations if `α` is. -/
 @[to_additive /-"`set α` is an `add_comm_monoid` under pointwise operations if `α` is. "-/]
 protected def comm_monoid [comm_monoid α] : comm_monoid (set α) :=
-{ mul_comm := λ _ _, set.mul_comm, ..set.monoid }
+{ ..set.monoid, ..set.comm_semigroup }
 
 localized "attribute [instance] set.mul_one_class set.add_zero_class set.semigroup set.add_semigroup
-  set.monoid set.add_monoid set.comm_monoid set.add_comm_monoid" in pointwise
+  set.comm_semigroup set.add_comm_semigroup set.monoid set.add_monoid set.comm_monoid
+  set.add_comm_monoid" in pointwise
 
 @[to_additive]
 lemma pow_mem_pow [monoid α] (ha : a ∈ s) (n : ℕ) :
@@ -1016,15 +1019,15 @@ localized "attribute [instance] set.mul_action_set set.add_action_set" in pointw
 
 section mul_hom
 
-variables [has_mul α] [has_mul β] (m : mul_hom α β) {s t : set α}
+variables [has_mul α] [has_mul β] [mul_hom_class F α β] (m : F) {s t : set α}
 
 @[to_additive]
-lemma image_mul : m '' (s * t) = m '' s * m '' t :=
-by { simp only [← image2_mul, image_image2, image2_image_left, image2_image_right, m.map_mul] }
+lemma image_mul : (m : α → β) '' (s * t) = m '' s * m '' t :=
+by simp only [← image2_mul, image_image2, image2_image_left, image2_image_right, map_mul m]
 
 @[to_additive]
-lemma preimage_mul_preimage_subset {s t : set β} : m ⁻¹' s * m ⁻¹' t ⊆ m ⁻¹' (s * t) :=
-by { rintros _ ⟨_, _, _, _, rfl⟩, exact ⟨_, _, ‹_›, ‹_›, (m.map_mul _ _).symm ⟩ }
+lemma preimage_mul_preimage_subset {s t : set β} : (m : α → β) ⁻¹' s * m ⁻¹' t ⊆ m ⁻¹' (s * t) :=
+by { rintros _ ⟨_, _, _, _, rfl⟩, exact ⟨_, _, ‹_›, ‹_›, (map_mul m _ _).symm ⟩ }
 
 instance set_semiring.no_zero_divisors : no_zero_divisors (set_semiring α) :=
 ⟨λ a b ab, a.eq_empty_or_nonempty.imp_right $ λ ha, b.eq_empty_or_nonempty.resolve_right $
@@ -1053,7 +1056,7 @@ def image_hom [monoid α] [monoid β] (f : α →* β) : set_semiring α →+* s
   map_zero' := image_empty _,
   map_one' := by simp only [← singleton_one, image_singleton, f.map_one],
   map_add' := image_union _,
-  map_mul' := λ _ _, image_mul f.to_mul_hom }
+  map_mul' := λ _ _, image_mul f }
 
 end monoid
 
@@ -1377,7 +1380,7 @@ lemma preimage_mul_right_one' [group α] :
 
 @[to_additive]
 protected lemma mul_comm [decidable_eq α] [comm_semigroup α] : s * t = t * s :=
-by exact_mod_cast @set.mul_comm _ (s : set α) t _
+by exact_mod_cast mul_comm (s : set α) t
 
 /-- `finset α` is a `mul_one_class` under pointwise operations if `α` is. -/
 @[to_additive /-"`finset α` is an `add_zero_class` under pointwise operations if `α` is."-/]

src/order/filter/pointwise.lean

@@ -5,179 +5,173 @@ Authors: Zhouhang Zhou
 -/
 import algebra.pointwise
 import order.filter.basic
+
 /-!
-# Pointwise operations on filters.
+# Pointwise operations on filters
+
+This file defines pointwise operations on filters. This is useful because usual algebraic operations
+distribute over pointwise operations. For example,
+* `(f₁ * f₂).map m  = f₁.map m * f₂.map m`
+* `𝓝 (x * y) = 𝓝 x * 𝓝 y`
+
+## Main declarations
+
+* `0` (`filter.has_zero`): Principal filter at `0 : α`.
+* `1` (`filter.has_one`): Principal filter at `1 : α`.
+* `f + g` (`filter.has_add`): Addition, filter generated by all `s + t` where `s ∈ f` and `t ∈ g`.
+* `f * g` (`filter.has_mul`): Multiplication, filter generated by all `s * t` where `s ∈ f` and
+  `t ∈ g`.
 
-The pointwise operations on filters have nice properties, such as
-  • `map m (f₁ * f₂) = map m f₁ * map m f₂`
-  • `𝓝 x * 𝓝 y = 𝓝 (x * y)`
+## TODO
 
+Add missing operations: subtraction/division, negation/inversion, scalar multiplication/addition
+
+## Tags
+
+filter multiplication, filter addition, pointwise addition, pointwise multiplication,
 -/
 
-open classical set
+open set
+open_locale pointwise
 
 universes u v w
-variables {α : Type u} {β : Type v} {γ : Type w}
-
-open_locale classical pointwise
+variables {F : Type*} {α : Type u} {β : Type v} {γ : Type w}
 
 namespace filter
-open set
 
-@[to_additive]
+/-- `1 : filter α` is the set of sets containing `1 : α`. -/
+@[to_additive "`0 : filter α` is the set of sets containing `0 : α`."]
 instance [has_one α] : has_one (filter α) := ⟨principal 1⟩
 
 @[simp, to_additive]
-lemma mem_one [has_one α] (s : set α) : s ∈ (1 : filter α) ↔ (1:α) ∈ s :=
-calc
-  s ∈ (1:filter α) ↔ 1 ⊆ s : iff.rfl
-  ... ↔ (1 : α) ∈ s : by simp
+lemma mem_one [has_one α] {s : set α} : s ∈ (1 : filter α) ↔ (1 : α) ∈ s := one_subset
 
 @[to_additive]
-instance [monoid α] : has_mul (filter α) := ⟨λf g,
-{ sets             := { s | ∃t₁ t₂, t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ * t₂ ⊆ s },
-  univ_sets        :=
-  begin
-    have h₁ : (∃x, x ∈ f) := ⟨univ, univ_sets f⟩,
-    have h₂ : (∃x, x ∈ g) := ⟨univ, univ_sets g⟩,
-    simpa using and.intro h₁ h₂
-  end,
+lemma one_mem_one [has_one α] : (1 : set α) ∈ (1 : filter α) := mem_principal_self _
+
+@[to_additive]
+instance [has_mul α] : has_mul (filter α) := ⟨λ f g,
+{ sets             := {s | ∃ t₁ t₂, t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ * t₂ ⊆ s},
+  univ_sets        := ⟨univ, univ, univ_sets _, univ_sets _, subset_univ _⟩,
   sets_of_superset := λx y hx hxy,
-  begin
-   rcases hx with ⟨t₁, ht₁, t₂, ht₂, t₁t₂⟩,
-   exact ⟨t₁, ht₁, t₂, ht₂, subset.trans t₁t₂ hxy⟩
-  end,
+    Exists₂.imp (λ t₁ t₂, and.imp_right $ and.imp_right $ λ h, subset.trans h hxy) hx,
   inter_sets       := λx y,
   begin
     simp only [exists_prop, mem_set_of_eq, subset_inter_iff],
     rintros ⟨s₁, s₂, hs₁, hs₂, s₁s₂⟩ ⟨t₁, t₂, ht₁, ht₂, t₁t₂⟩,
     exact ⟨s₁ ∩ t₁, s₂ ∩ t₂, inter_sets f hs₁ ht₁, inter_sets g hs₂ ht₂,
-    subset.trans (mul_subset_mul (inter_subset_left _ _) (inter_subset_left _ _)) s₁s₂,
-    subset.trans (mul_subset_mul (inter_subset_right _ _) (inter_subset_right _ _)) t₁t₂⟩,
+      (mul_subset_mul (inter_subset_left _ _) $ inter_subset_left _ _).trans s₁s₂,
+      (mul_subset_mul (inter_subset_right _ _) $ inter_subset_right _ _).trans t₁t₂⟩,
   end }⟩
 
 @[to_additive]
-lemma mem_mul [monoid α] {f g : filter α} {s : set α} :
-  s ∈ f * g ↔ ∃t₁ t₂, t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ * t₂  ⊆ s := iff.rfl
+lemma mem_mul [has_mul α] {f g : filter α} {s : set α} :
+  s ∈ f * g ↔ ∃ t₁ t₂, t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ * t₂ ⊆ s := iff.rfl
 
 @[to_additive]
-lemma mul_mem_mul [monoid α] {f g : filter α} {s t : set α} (hs : s ∈ f) (ht : t ∈ g) :
-  s * t ∈ f * g := ⟨_, _, hs, ht, subset.refl _⟩
+lemma mul_mem_mul [has_mul α] {f g : filter α} {s t : set α} (hs : s ∈ f) (ht : t ∈ g) :
+  s * t ∈ f * g := ⟨_, _, hs, ht, subset.rfl⟩
 
 @[to_additive]
-protected lemma mul_le_mul [monoid α] {f₁ f₂ g₁ g₂ : filter α} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) :
+protected lemma mul_le_mul [has_mul α] {f₁ f₂ g₁ g₂ : filter α} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) :
   f₁ * g₁ ≤ f₂ * g₂ := assume _ ⟨s, t, hs, ht, hst⟩, ⟨s, t, hf hs, hg ht, hst⟩
 
 @[to_additive]
-lemma ne_bot.mul [monoid α] {f g : filter α} : ne_bot f → ne_bot g → ne_bot (f * g) :=
+lemma ne_bot.mul [has_mul α] {f g : filter α} : ne_bot f → ne_bot g → ne_bot (f * g) :=
 begin
   simp only [forall_mem_nonempty_iff_ne_bot.symm],
   rintros hf hg s ⟨a, b, ha, hb, ab⟩,
   exact ((hf a ha).mul (hg b hb)).mono ab
 end
 
 @[to_additive]
-protected lemma mul_assoc [monoid α] (f g h : filter α) : f * g * h = f * (g * h) :=
-begin
-  ext s, split,
-  { rintros ⟨a, b, ⟨a₁, a₂, ha₁, ha₂, a₁a₂⟩, hb, ab⟩,
-    refine ⟨a₁, a₂ * b, ha₁, mul_mem_mul ha₂ hb, _⟩, rw [← mul_assoc],
-    calc
-      a₁ * a₂ * b ⊆ a * b : mul_subset_mul a₁a₂ (subset.refl _)
-      ...         ⊆ s     : ab },
-  { rintros ⟨a, b, ha, ⟨b₁, b₂, hb₁, hb₂, b₁b₂⟩, ab⟩,
-    refine ⟨a * b₁, b₂, mul_mem_mul ha hb₁, hb₂, _⟩, rw [mul_assoc],
-    calc
-      a * (b₁ * b₂) ⊆ a * b : mul_subset_mul (subset.refl _) b₁b₂
-      ...           ⊆ s     : ab }
-end
+instance [semigroup α] : semigroup (filter α) :=
+{ mul := (*),
+  mul_assoc := λ f g h, filter.ext $ λ s, begin
+    split,
+    { rintro ⟨a, b, ⟨a₁, a₂, ha₁, ha₂, a₁a₂⟩, hb, ab⟩,
+      refine ⟨a₁, a₂ * b, ha₁, mul_mem_mul ha₂ hb, _⟩,
+      rw ←mul_assoc,
+      exact (mul_subset_mul a₁a₂ subset.rfl).trans ab },
+    { rintro ⟨a, b, ha, ⟨b₁, b₂, hb₁, hb₂, b₁b₂⟩, ab⟩,
+      refine ⟨a * b₁, b₂, mul_mem_mul ha hb₁, hb₂, _⟩,
+      rw mul_assoc,
+      exact (mul_subset_mul subset.rfl b₁b₂).trans ab }
+  end }
 
 @[to_additive]
-protected lemma one_mul [monoid α] (f : filter α) : 1 * f = f :=
-begin
-  ext s, split,
-  { rintros ⟨t₁, t₂, ht₁, ht₂, t₁t₂⟩,
-    refine mem_of_superset (mem_of_superset ht₂ _) t₁t₂,
-    assume x hx,
-    exact ⟨1, x, by rwa [← mem_one], hx, one_mul _⟩ },
-  { assume hs, refine ⟨(1:set α), s, mem_principal_self _, hs, by simp only [one_mul]⟩ }
-end
+instance [comm_semigroup α] : comm_semigroup (filter α) :=
+{ mul_comm := λ f g, filter.ext $ λ s, exists_comm.trans $ exists₂_congr $ λ t₁ t₂,
+    by rw [and.left_comm, mul_comm],
+  ..filter.semigroup }
 
 @[to_additive]
-protected lemma mul_one [monoid α] (f : filter α) : f * 1 = f :=
-begin
-  ext s, split,
-  { rintros ⟨t₁, t₂, ht₁, ht₂, t₁t₂⟩,
-    refine mem_of_superset (mem_of_superset ht₁ _) t₁t₂,
-    assume x hx,
-    exact ⟨x, 1, hx, by rwa [← mem_one], mul_one _⟩ },
-  { assume hs,
-    refine ⟨s, (1:set α), hs, mem_principal_self _, by simp only [mul_one]⟩ }
-end
+instance [mul_one_class α] : mul_one_class (filter α) :=
+{ one := 1,
+  mul := (*),
+  one_mul := λ f, filter.ext $ λ s, begin
+    refine ⟨_, λ hs,  ⟨1, s, one_mem_one, hs, (one_mul _).subset⟩⟩,
+    rintro ⟨t₁, t₂, ht₁, ht₂, t₁t₂⟩,
+    exact mem_of_superset ht₂ ((subset_mul_right _ $ mem_one.1 ht₁).trans t₁t₂),
+  end,
+  mul_one := λ f, filter.ext $ λ s, begin
+    refine ⟨_, λ hs, ⟨s, 1, hs, one_mem_one, (mul_one _).subset⟩⟩,
+    rintro ⟨t₁, t₂, ht₁, ht₂, t₁t₂⟩,
+    exact mem_of_superset ht₁ ((subset_mul_left _ $ mem_one.1 ht₂).trans t₁t₂),
+  end }
 
-@[to_additive filter.add_monoid]
-instance [monoid α] : monoid (filter α) :=
-{ mul_assoc := filter.mul_assoc,
-  one_mul := filter.one_mul,
-  mul_one := filter.mul_one,
-  .. filter.has_mul,
-  .. filter.has_one }
+@[to_additive]
+instance [monoid α] : monoid (filter α) := { ..filter.mul_one_class, ..filter.semigroup }
+
+@[to_additive]
+instance [comm_monoid α] : comm_monoid (filter α) :=
+{ ..filter.mul_one_class, ..filter.comm_semigroup }
 
 section map
 
-variables [monoid α] [monoid β] {f : filter α} (m : mul_hom α β) (φ : α →* β)
+variables [monoid α] [monoid β] {f f₁ f₂ : filter α}
 
 @[to_additive]
-protected lemma map_mul {f₁ f₂ : filter α} : map m (f₁ * f₂) = map m f₁ * map m f₂ :=
+protected lemma map_mul [mul_hom_class F α β] (m : F) : (f₁ * f₂).map m = f₁.map m * f₂.map m :=
 begin
   ext s,
-  simp only [mem_mul], split,
+  split,
   { rintro ⟨t₁, t₂, ht₁, ht₂, t₁t₂⟩,
     have : m '' (t₁ * t₂) ⊆ s := subset.trans (image_subset m t₁t₂) (image_preimage_subset _ _),
-    refine ⟨m '' t₁, m '' t₂, image_mem_map ht₁, image_mem_map ht₂, _⟩,
-    rwa ← image_mul m },
+    exact ⟨m '' t₁, m '' t₂, image_mem_map ht₁, image_mem_map ht₂, by rwa ← image_mul m⟩ },
   { rintro ⟨t₁, t₂, ht₁, ht₂, t₁t₂⟩,
     refine ⟨m ⁻¹' t₁, m ⁻¹' t₂, ht₁, ht₂, image_subset_iff.1 _⟩,
     rw image_mul m,
-    exact subset.trans
-      (mul_subset_mul (image_preimage_subset _ _) (image_preimage_subset _ _)) t₁t₂ },
+    exact (mul_subset_mul (image_preimage_subset _ _) $ image_preimage_subset _ _).trans t₁t₂ }
 end
 
-@[to_additive]
-protected lemma map_one : map φ (1:filter α) = 1 :=
+@[simp, to_additive]
+protected lemma map_one [one_hom_class F α β] (φ : F) : map φ 1 = 1 :=
 le_antisymm
-  (le_principal_iff.2 $ mem_map_iff_exists_image.2 ⟨(1:set α), by simp,
-    by { assume x, simp [φ.map_one] }⟩)
-  (le_map $ assume s hs,
-   begin
-     simp only [mem_one],
-     exact ⟨(1:α), (mem_one s).1 hs, φ.map_one⟩
-   end)
+  (le_principal_iff.2 $ mem_map_iff_exists_image.2 ⟨1, one_mem_one, λ x, by simp [map_one φ]⟩)
+  (le_map $ λ s hs, mem_one.2 ⟨1, mem_one.1 hs, map_one φ⟩)
 
 /-- If `φ : α →* β` then `map_monoid_hom φ` is the monoid homomorphism
 `filter α →* filter β` induced by `map φ`. -/
 @[to_additive "If `φ : α →+ β` then `map_add_monoid_hom φ` is the monoid homomorphism
 `filter α →+ filter β` induced by `map φ`."]
-def map_monoid_hom : filter α →* filter β :=
+def map_monoid_hom [monoid_hom_class F α β] (φ : F) : filter α →* filter β :=
 { to_fun := map φ,
   map_one' := filter.map_one φ,
-  map_mul' := λ _ _, filter.map_mul φ.to_mul_hom }
+  map_mul' := λ _ _, filter.map_mul φ }
 
 -- The other direction does not hold in general.
 @[to_additive]
-lemma comap_mul_comap_le {f₁ f₂ : filter β} :
-  comap m f₁ * comap m f₂ ≤ comap m (f₁ * f₂) :=
-begin
-  rintros s ⟨t, ⟨t₁, t₂, ht₁, ht₂, t₁t₂⟩, mt⟩,
-  refine ⟨m ⁻¹' t₁, m ⁻¹' t₂, ⟨t₁, ht₁, subset.refl _⟩, ⟨t₂, ht₂, subset.refl _⟩, _⟩,
-  have := subset.trans (preimage_mono t₁t₂) mt,
-  exact subset.trans (preimage_mul_preimage_subset _) this
-end
+lemma comap_mul_comap_le [mul_hom_class F α β] (m : F) {f₁ f₂ : filter β} :
+  f₁.comap m * f₂.comap m ≤ (f₁ * f₂).comap m  :=
+λ s ⟨t, ⟨t₁, t₂, ht₁, ht₂, t₁t₂⟩, mt⟩,
+  ⟨m ⁻¹' t₁, m ⁻¹' t₂, ⟨t₁, ht₁, subset.rfl⟩, ⟨t₂, ht₂, subset.rfl⟩,
+    (preimage_mul_preimage_subset _).trans $ (preimage_mono t₁t₂).trans mt⟩
 
 @[to_additive]
-lemma tendsto.mul_mul {f₁ g₁ : filter α} {f₂ g₂ : filter β} :
+lemma tendsto.mul_mul [mul_hom_class F α β] (m : F) {f₁ g₁ : filter α} {f₂ g₂ : filter β} :
   tendsto m f₁ f₂ → tendsto m g₁ g₂ → tendsto m (f₁ * g₁) (f₂ * g₂) :=
-assume hf hg, by { rw [tendsto, filter.map_mul m], exact filter.mul_le_mul hf hg }
+λ hf hg, (filter.map_mul m).trans_le $ filter.mul_le_mul hf hg
 
 end map
 

src/ring_theory/graded_algebra/homogeneous_ideal.lean

@@ -341,8 +341,7 @@ begin
   rw ideal.is_homogeneous.iff_exists at HI HJ ⊢,
   obtain ⟨⟨s₁, rfl⟩, ⟨s₂, rfl⟩⟩ := ⟨HI, HJ⟩,
   rw ideal.span_mul_span',
-  refine ⟨s₁ * s₂, congr_arg _ _⟩,
-  exact (set.image_mul (submonoid.subtype _).to_mul_hom).symm,
+  exact ⟨s₁ * s₂, congr_arg _ $ (set.image_mul (homogeneous_submonoid 𝒜).subtype).symm⟩,
 end
 
 variables {𝒜}