feat(data/(d)finsupp,fintype,fun_like): add fintype and (in)finite in…

…stances (#15725)




Co-authored-by: Anne Baanen <t.baanen@vu.nl>
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/data/dfinsupp/basic.lean

@@ -551,6 +551,12 @@ begin
     { rw [hi, hj, dfinsupp.single_zero, dfinsupp.single_zero], }, },
 end
 
+/-- `dfinsupp.single a b` is injective in `a`. For the statement that it is injective in `b`, see
+`dfinsupp.single_injective` -/
+lemma single_left_injective {b : Π (i : ι), β i} (h : ∀ i, b i ≠ 0) :
+  function.injective (λ i, single i (b i) : ι → Π₀ i, β i) :=
+λ a a' H, (((single_eq_single_iff _ _ _ _).mp H).resolve_right $ λ hb, h _ hb.1).left
+
 @[simp] lemma single_eq_zero {i : ι} {xi : β i} : single i xi = 0 ↔ xi = 0 :=
 begin
   rw [←single_zero i, single_eq_single_iff],
@@ -1960,3 +1966,32 @@ add_monoid_hom.congr_fun (comp_lift_add_hom h.to_add_monoid_hom g) f
 end add_equiv
 
 end
+
+section finite_infinite
+
+instance dfinsupp.fintype {ι : Sort*} {π : ι → Sort*} [decidable_eq ι] [Π i, has_zero (π i)]
+  [fintype ι] [∀ i, fintype (π i)] :
+  fintype (Π₀ i, π i) :=
+fintype.of_equiv (Π i, π i) dfinsupp.equiv_fun_on_fintype.symm
+
+instance dfinsupp.infinite_of_left {ι : Sort*} {π : ι → Sort*}
+  [∀ i, nontrivial (π i)] [Π i, has_zero (π i)] [infinite ι] :
+  infinite (Π₀ i, π i) :=
+by letI := classical.dec_eq ι; choose m hm using (λ i, exists_ne (0 : π i)); exact
+infinite.of_injective _ (dfinsupp.single_left_injective hm)
+
+/-- See `dfinsupp.infinite_of_right` for this in instance form, with the drawback that
+it needs all `π i` to be infinite. -/
+lemma dfinsupp.infinite_of_exists_right {ι : Sort*} {π : ι → Sort*}
+  (i : ι) [infinite (π i)] [Π i, has_zero (π i)] :
+  infinite (Π₀ i, π i) :=
+by letI := classical.dec_eq ι; exact
+infinite.of_injective (λ j, dfinsupp.single i j) dfinsupp.single_injective
+
+/-- See `dfinsupp.infinite_of_exists_right` for the case that only one `π ι` is infinite. -/
+instance dfinsupp.infinite_of_right {ι : Sort*} {π : ι → Sort*}
+  [∀ i, infinite (π i)] [Π i, has_zero (π i)] [nonempty ι] :
+  infinite (Π₀ i, π i) :=
+dfinsupp.infinite_of_exists_right (classical.arbitrary ι)
+
+end finite_infinite

src/data/finsupp/fintype.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2022 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen, Alex J. Best
+-/
+import data.finsupp.defs
+import data.fintype.basic
+
+/-!
+
+# Finiteness and infiniteness of `finsupp`
+
+Some lemmas on the combination of `finsupp`, `fintype` and `infinite`.
+
+-/
+
+noncomputable instance finsupp.fintype {ι π : Sort*} [decidable_eq ι] [has_zero π]
+  [fintype ι] [fintype π] :
+  fintype (ι →₀ π) :=
+fintype.of_equiv _ finsupp.equiv_fun_on_fintype.symm
+
+instance finsupp.infinite_of_left {ι π : Sort*} [nontrivial π] [has_zero π] [infinite ι] :
+  infinite (ι →₀ π) :=
+let ⟨m, hm⟩ := exists_ne (0 : π) in infinite.of_injective _ $ finsupp.single_left_injective hm
+
+instance finsupp.infinite_of_right {ι π : Sort*} [infinite π] [has_zero π] [nonempty ι] :
+  infinite (ι →₀ π) :=
+infinite.of_injective (λ i, finsupp.single (classical.arbitrary ι) i)
+  (finsupp.single_injective (classical.arbitrary ι))

src/data/fintype/basic.lean

@@ -2169,6 +2169,36 @@ begin
   exact H'.false
 end
 
+instance pi.infinite_of_left {ι : Sort*} {π : ι → Sort*} [∀ i, nontrivial $ π i]
+  [infinite ι] : infinite (Π i : ι, π i) :=
+begin
+  choose m n hm using λ i, exists_pair_ne (π i),
+  refine infinite.of_injective (λ i, m.update i (n i)) (λ x y h, not_not.1 $ λ hne, _),
+  simp_rw [update_eq_iff, update_noteq hne] at h,
+  exact (hm x h.1.symm).elim,
+end
+
+/-- If at least one `π i` is infinite and the rest nonempty, the pi type of all `π` is infinite. -/
+lemma pi.infinite_of_exists_right {ι : Type*} {π : ι → Type*} (i : ι)
+  [infinite $ π i] [∀ i, nonempty $ π i] :
+  infinite (Π i : ι, π i) :=
+let ⟨m⟩ := @pi.nonempty ι π _ in infinite.of_injective _ (update_injective m i)
+
+/-- See `pi.infinite_of_exists_right` for the case that only one `π i` is infinite. -/
+instance pi.infinite_of_right {ι : Sort*} {π : ι → Sort*} [∀ i, infinite $ π i] [nonempty ι] :
+  infinite (Π i : ι, π i) :=
+pi.infinite_of_exists_right (classical.arbitrary ι)
+
+/-- Non-dependent version of `pi.infinite_of_left`. -/
+instance function.infinite_of_left {ι π : Sort*} [nontrivial π]
+  [infinite ι] : infinite (ι → π) :=
+pi.infinite_of_left
+
+/-- Non-dependent version of `pi.infinite_of_exists_right` and `pi.infinite_of_right`. -/
+instance function.infinite_of_right {ι π : Sort*} [infinite π] [nonempty ι] :
+  infinite (ι → π) :=
+pi.infinite_of_right
+
 namespace infinite
 
 private noncomputable def nat_embedding_aux (α : Type*) [infinite α] : ℕ → α

src/data/fun_like/fintype.lean

@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2022 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+-/
+
+import data.finite.basic
+import data.fintype.basic
+import data.fun_like.basic
+
+/-!
+# Finiteness of `fun_like` types
+
+We show a type `F` with a `fun_like F α β` is finite if both `α` and `β` are finite.
+This corresponds to the following two pairs of declarations:
+
+ * `fun_like.fintype` is a definition stating all `fun_like`s are finite if their domain and
+   codomain are.
+ * `fun_like.finite` is a lemma stating all `fun_like`s are finite if their domain and
+   codomain are.
+ * `fun_like.fintype'` is a non-dependent version of `fun_like.fintype` and
+ * `fun_like.finite` is a non-dependent version of `fun_like.finite`, because dependent instances
+   are harder to infer.
+
+You can use these to produce instances for specific `fun_like` types.
+(Although there might be options for `fintype` instances with better definitional behaviour.)
+They can't be instances themselves since they can cause loops.
+-/
+
+section type
+
+variables (F G : Type*) {α γ : Type*} {β : α → Type*} [fun_like F α β] [fun_like G α (λ _, γ)]
+
+/-- All `fun_like`s are finite if their domain and codomain are.
+
+This is not an instance because specific `fun_like` types might have a better-suited definition.
+
+See also `fun_like.finite`.
+-/
+noncomputable def fun_like.fintype [decidable_eq α] [fintype α] [Π i, fintype (β i)] : fintype F :=
+fintype.of_injective _ fun_like.coe_injective
+
+/-- All `fun_like`s are finite if their domain and codomain are.
+
+Non-dependent version of `fun_like.fintype` that might be easier to infer.
+This is not an instance because specific `fun_like` types might have a better-suited definition.
+-/
+noncomputable def fun_like.fintype' [decidable_eq α] [fintype α] [fintype γ] : fintype G :=
+fun_like.fintype G
+
+end type
+
+section sort
+
+variables (F G : Sort*) {α γ : Sort*} {β : α → Sort*} [fun_like F α β] [fun_like G α (λ _, γ)]
+
+/-- All `fun_like`s are finite if their domain and codomain are.
+
+Can't be an instance because it can cause infinite loops.
+-/
+lemma fun_like.finite [finite α] [∀ i, finite (β i)] : finite F :=
+finite.of_injective _ fun_like.coe_injective
+
+/-- All `fun_like`s are finite if their domain and codomain are.
+
+Non-dependent version of `fun_like.finite` that might be easier to infer.
+Can't be an instance because it can cause infinite loops.
+-/
+lemma fun_like.finite' [finite α] [finite γ] : finite G :=
+fun_like.finite G
+
+end sort

src/data/mv_polynomial/cardinal.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Chris Hughes, Junyan Xu. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Junyan Xu
 -/
+import data.finsupp.fintype
 import data.mv_polynomial.equiv
 import set_theory.cardinal.ordinal
 /-!
@@ -25,11 +26,8 @@ variables {σ : Type u} {R : Type v} [comm_semiring R]
 
 @[simp] lemma cardinal_mk_eq_max_lift [nonempty σ] [nontrivial R] :
   #(mv_polynomial σ R) = max (max (cardinal.lift.{u} $ #R) $ cardinal.lift.{v} $ #σ) ℵ₀ :=
-begin
-  haveI : infinite (σ →₀ ℕ) := infinite_iff.2 ((le_max_right _ _).trans (mk_finsupp_nat σ).ge),
-  refine (mk_finsupp_lift_of_infinite _ R).trans _,
-  rw [mk_finsupp_nat, max_assoc, lift_max, lift_aleph_0, max_comm],
-end
+(mk_finsupp_lift_of_infinite _ R).trans $
+by rw [mk_finsupp_nat, max_assoc, lift_max, lift_aleph_0, max_comm]
 
 @[simp] lemma cardinal_mk_eq_lift [is_empty σ] : #(mv_polynomial σ R) = cardinal.lift.{u} (#R) :=
 ((is_empty_ring_equiv R σ).to_equiv.trans equiv.ulift.{u}.symm).cardinal_eq