feat(Algebra/Order/Antidiagonal): connect Finset.HasAntidiagonal with Filter.TendstoCofinite

Mathlib/Algebra/Order/Antidiag/Prod.lean

@@ -60,8 +60,8 @@ open Function
 
 namespace Finset
 
-/-- The class of additive monoids with an antidiagonal. -/
-class HasAntidiagonal (A : Type*) [AddMonoid A] where
+/-- The class of additive magmas with an antidiagonal. -/
+class HasAntidiagonal (A : Type*) [Add A] where
   /-- The antidiagonal of an element `n` is the finset of pairs `(i, j)` such that
   `i + j = n`. -/
   antidiagonal : A → Finset (A × A)
@@ -72,8 +72,8 @@ export HasAntidiagonal (antidiagonal mem_antidiagonal)
 
 attribute [simp] mem_antidiagonal
 
-/-- The class of (multiplicative) monoids with a mulAntidiagonal. -/
-class HasMulAntidiagonal (A : Type*) [Monoid A] where
+/-- The class of (multiplicative) magmas with a mulAntidiagonal. -/
+class HasMulAntidiagonal (A : Type*) [Mul A] where
   /-- The mulAntidiagonal of an element `n` is the finset of pairs `(i, j)` such that
   `i * j = n`. -/
   mulAntidiagonal : A → Finset (A × A)
@@ -92,38 +92,42 @@ namespace HasMulAntidiagonal
 
 /-- All `HasMulAntidiagonal` instances are equal -/
 @[to_additive /-- All `HasAntidiagonal` instances are equal -/]
-instance [Monoid A] : Subsingleton (HasMulAntidiagonal A) where
+instance [Mul A] : Subsingleton (HasMulAntidiagonal A) where
   allEq := by
     rintro ⟨a, ha⟩ ⟨b, hb⟩
     congr with n xy
     rw [ha, hb]
 
 @[to_additive]
-lemma nonempty_antidiagonal {M : Type*} [Monoid M] [Finset.HasMulAntidiagonal M] (a : M) :
-    (Finset.mulAntidiagonal a).Nonempty :=
+lemma coe_mulAntidiagonal_eq_preimage_singleton [Mul A] [HasMulAntidiagonal A] (a : A) :
+    mulAntidiagonal a = ((fun (p : A × A) ↦ p.1 * p.2) ⁻¹' {a}) := by
+  ext; simp
+
+@[to_additive]
+lemma nonempty_antidiagonal {M : Type*} [MulOneClass M] [HasMulAntidiagonal M] (a : M) :
+    (mulAntidiagonal a).Nonempty :=
   ⟨(1, a), by simp⟩
 
 -- The goal of this lemma is to allow to rewrite mulAntidiagonal/antidiagonal
 -- when the decidability instances obfuscate Lean
 set_option linter.overlappingInstances false in
 @[to_additive]
-lemma congr (A : Type*) [Monoid A]
-    [H1 : HasMulAntidiagonal A] [H2 : HasMulAntidiagonal A] :
+lemma congr (A : Type*) [Mul A] [H1 : HasMulAntidiagonal A] [H2 : HasMulAntidiagonal A] :
     H1.mulAntidiagonal = H2.mulAntidiagonal := by congr!; subsingleton
 
 @[to_additive]
-theorem swap_mem_mulAntidiagonal [CommMonoid A] [HasMulAntidiagonal A] {n : A} {xy : A × A} :
+theorem swap_mem_mulAntidiagonal [CommMagma A] [HasMulAntidiagonal A] {n : A} {xy : A × A} :
     xy.swap ∈ mulAntidiagonal n ↔ xy ∈ mulAntidiagonal n := by
   simp [mul_comm]
 
 @[to_additive (attr := simp) map_prodComm_antidiagonal]
-theorem map_prodComm_mulAntidiagonal [CommMonoid A] [HasMulAntidiagonal A] {n : A} :
+theorem map_prodComm_mulAntidiagonal [CommMagma A] [HasMulAntidiagonal A] {n : A} :
     (mulAntidiagonal n).map (Equiv.prodComm A A) = mulAntidiagonal n :=
   Finset.ext fun ⟨a, b⟩ => by simp [mul_comm]
 
 /-- See also `Finset.map_prodComm_mulAntidiagonal`. -/
 @[to_additive (attr := simp)]
-theorem map_swap_mulAntidiagonal [CommMonoid A] [HasMulAntidiagonal A] {n : A} :
+theorem map_swap_mulAntidiagonal [CommMagma A] [HasMulAntidiagonal A] {n : A} :
     (mulAntidiagonal n).map ⟨Prod.swap, Prod.swap_injective⟩ = mulAntidiagonal n :=
   map_prodComm_mulAntidiagonal
 
@@ -232,7 +236,7 @@ namespace HasMulAntidiagonal
 @[to_additive (attr := simps) sigmaAntidiagonalEquivProd
 /-- The disjoint union of antidiagonals `Σ (n : A), antidiagonal n` is equivalent to the
   product `A × A`. This is such an equivalence, obtained by mapping `(n, (k, l))` to `(k, l)`. -/]
-def sigmaMulAntidiagonalEquivProd [Monoid A] [HasMulAntidiagonal A] :
+def sigmaMulAntidiagonalEquivProd [Mul A] [HasMulAntidiagonal A] :
     (Σ n : A, mulAntidiagonal n) ≃ A × A where
   toFun x := x.2
   invFun x := ⟨x.1 * x.2, x, mem_mulAntidiagonal.mpr rfl⟩
@@ -244,15 +248,15 @@ def sigmaMulAntidiagonalEquivProd [Monoid A] [HasMulAntidiagonal A] :
 section
 
 variable {A : Type*}
-  [CommMonoid A] [PartialOrder A] [CanonicallyOrderedMul A]
+  [CommMagma A] [PartialOrder A] [CanonicallyOrderedMul A]
   [LocallyFiniteOrderBot A] [DecidableEq A]
 
-/-- In a canonically ordered multiplicative monoid, the mulAntidiagonal can be constructed by
+/-- In a canonically ordered multiplicative magma, the mulAntidiagonal can be constructed by
 filtering.
 
 Note that this is not an instance, as for sometimes a more efficient algorithm is available. -/
 @[to_additive
-/-- In a canonically ordered additive monoid, the antidiagonal can be construct by filtering.
+/-- In a canonically ordered additive magma, the antidiagonal can be construct by filtering.
 
 Note that this is not an instance, as for some times a more efficient algorithm is available. -/]
 abbrev mulAntidiagonalOfLocallyFinite : HasMulAntidiagonal A where
@@ -268,7 +272,7 @@ section Multiplicative
 
 open Multiplicative
 
-variable {A : Type*} [AddMonoid A] [HasAntidiagonal A]
+variable {A : Type*} [Add A] [HasAntidiagonal A]
 
 instance : HasMulAntidiagonal (Multiplicative A) where
   mulAntidiagonal a :=

Mathlib/Algebra/Order/Antidiag/Tendsto.lean

@@ -7,23 +7,29 @@ module
 
 public import Mathlib.Algebra.Group.Pointwise.Set.Finite
 public import Mathlib.Algebra.Order.Antidiag.Prod
-public import Mathlib.Order.Filter.Cofinite
+public import Mathlib.Order.Filter.TendstoCofinite
 
 /-!
 # Antidiagonal tendsto
 
-`tendsto_sup'_antidiagonal_cofinite`: If a function `f : M × M → R` on a Finset `M`, that has the
-  antidiagonal propertry,  tends to to a filter `F` under the cofinite filter then so does the
-  function assigning to `x : M` its supremum of its antidiagonal.
--/
+`Finset.HasAntidiagonal.tendsto_sup'_antidiagonal_cofinite`:
+  If a function `f : M × M → R` on a Finset `M`, that has the antidiagonal propertry,
+  tends to a filter `F` under the cofinite filter then so does
+  the function assigning to `x : M` its supremum of its antidiagonal.
 
-@[expose] public section
+`Finset.HasMulAntidiagonal.tendstoCofinite_mul`:
+  When a magma satisfies the `HasMulAntidiagonal` property, its multiplication map has
+  finite fibers.
 
-namespace Finset.HasAntidiagonal
+-/
+
+public section
 
 open Filter
 
-variable {M R : Type*} [AddMonoid M] [HasAntidiagonal M] {f : M × M → R} [LinearOrder R]
+namespace Finset.HasAntidiagonal
+
+variable {M R : Type*} [AddZeroClass M] [HasAntidiagonal M] {f : M × M → R} [LinearOrder R]
   {F : Filter R}
 
 lemma tendsto_sup'_antidiagonal_cofinite (hf : Tendsto f cofinite F) : Tendsto
@@ -37,3 +43,20 @@ lemma tendsto_sup'_antidiagonal_cofinite (hf : Tendsto f cofinite F) : Tendsto
   exact Set.add_mem_add (by simpa using ⟨i.2, e ▸ hx⟩) (by simpa using ⟨i.1, e ▸ hx⟩)
 
 end Finset.HasAntidiagonal
+
+namespace Finset.HasMulAntidiagonal
+
+variable {N : Type*} [Mul N] [HasMulAntidiagonal N]
+
+/-- When a magma satisfies the `HasMulAntidiagonal` property, its multiplication map has
+finite fibers.
+
+For the reverse implication, see `Filter.TendstoCofinite.hasMulAntidiagonal`. -/
+@[to_additive /-- When an additive magma satisfies the `HasMulAntidiagonal` property,
+its addition map has finite fibers.
+
+For the reverse implication, see `Filter.TendstoCofinite.hasAntidiagonal`-/]
+instance tendstoCofinite_mul : TendstoCofinite fun (p : N × N) ↦ p.1 * p.2 := by
+  simp [tendstoCofinite_iff_finite_preimage_singleton, ← coe_mulAntidiagonal_eq_preimage_singleton]
+
+end Finset.HasMulAntidiagonal

Mathlib/Order/Filter/TendstoCofinite.lean

@@ -62,25 +62,31 @@ theorem tendstoCofinite_iff_finite_preimage_singleton : TendstoCofinite f ↔
 variable {f} in
 lemma tendstoCofinite_of_injective (h : f.Injective) : TendstoCofinite f := ⟨h.tendsto_cofinite⟩
 
-@[instance]
-lemma tendstoCofinite_of_finite [Finite α] : TendstoCofinite f :=
+instance tendstoCofinite_of_finite [Finite α] : TendstoCofinite f :=
   (tendstoCofinite_iff_finite_preimage_singleton f).mpr fun b ↦ Set.toFinite (f ⁻¹' {b})
 
 namespace TendstoCofinite
 
-@[instance]
-lemma comp [TendstoCofinite g] [TendstoCofinite f] : TendstoCofinite (g ∘ f) :=
+instance comp [TendstoCofinite g] [TendstoCofinite f] : TendstoCofinite (g ∘ f) :=
   (tendstoCofinite_iff_finite_preimage_singleton _).mpr (fun r ↦ by
     simpa using! TendstoCofinite.finite_preimage f (TendstoCofinite.finite_preimage g (by simp)))
 
-@[instance]
-lemma id : TendstoCofinite (id : α → α) := by simp [tendstoCofinite_iff_finite_preimage_singleton]
+instance id : TendstoCofinite (id : α → α) := by
+  simp [tendstoCofinite_iff_finite_preimage_singleton]
 
-@[instance]
-lemma embedding (e : α ↪ β) : TendstoCofinite e := ⟨e.injective.tendsto_cofinite⟩
+instance embedding (e : α ↪ β) : TendstoCofinite e := ⟨e.injective.tendsto_cofinite⟩
 
-@[instance]
-lemma equiv (e : α ≃ β) : TendstoCofinite e := ⟨e.injective.tendsto_cofinite⟩
+instance equiv (e : α ≃ β) : TendstoCofinite e := ⟨e.injective.tendsto_cofinite⟩
+
+open Finset in
+/-- Noncomputably constructs `HasMulAntidiagonal` data from the assumption that
+the multiplication map has finite fibers. -/
+@[to_additive /-- Noncomputably constructs `HasMulAntidiagonal` data from the assumption that
+the addition map has finite fibers. -/]
+noncomputable abbrev hasMulAntidiagonal {N : Type*} [Monoid N]
+    [TendstoCofinite fun (p : N × N) ↦ p.1 * p.2] : HasMulAntidiagonal N where
+  mulAntidiagonal a := (finite_preimage_singleton (fun (p : N × N) ↦ p.1 * p.2) a).toFinset
+  mem_mulAntidiagonal := by simp
 
 variable [TendstoCofinite f]
 
@@ -106,8 +112,7 @@ end TendstoCofinite
 
 end Filter
 
-@[instance]
-theorem Finsupp.mapDomain_tendstoCofinite [TendstoCofinite f] :
+instance Finsupp.mapDomain_tendstoCofinite [TendstoCofinite f] :
     TendstoCofinite (mapDomain (M := ℕ) f) := by
   classical
   refine (tendstoCofinite_iff_finite_preimage_singleton _).mpr fun x ↦ ?_