diff --git a/Mathlib/Algebra/Order/Antidiag/Prod.lean b/Mathlib/Algebra/Order/Antidiag/Prod.lean index 398a5813e4bc4f..17179a96e9ca9f 100644 --- a/Mathlib/Algebra/Order/Antidiag/Prod.lean +++ b/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 := diff --git a/Mathlib/Algebra/Order/Antidiag/Tendsto.lean b/Mathlib/Algebra/Order/Antidiag/Tendsto.lean index 34a9de60c58691..ceab77bb6b1231 100644 --- a/Mathlib/Algebra/Order/Antidiag/Tendsto.lean +++ b/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 diff --git a/Mathlib/Order/Filter/TendstoCofinite.lean b/Mathlib/Order/Filter/TendstoCofinite.lean index ecec915ed07312..708b671a63be80 100644 --- a/Mathlib/Order/Filter/TendstoCofinite.lean +++ b/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 ↦ ?_