Cardinalities of products with finitely many nontrivial factors and of ranges

Mathlib's Nat.card_pi computes the cardinality of a product ∀ i, X i over a finite index type. This file allows an arbitrary index type, provided that all factors outside a finite set s have exactly one element: the product then has the cardinality of its factors over s. Such products arise as restricted-product-like objects, for instance a cohomology group of a product of modules in which only finitely many factors contribute.

The file also compares the ranges of two maps f and f' with e' ∘ f = f' ∘ e, where e is surjective and e' is injective on the range of f: e' maps the range of f bijectively onto the range of f'. For instance, two linear maps intertwined by linear equivalences on the source and on the target have ranges of the same cardinality; this is a counting step of exact-sequence arguments.

Main results

• Nat.card_pi_eq_prod_of_card_eq_one: Nat.card (∀ i, X i) = ∏ i ∈ s, Nat.card (X i) when every factor outside s has cardinality one.
• Nat.card_range_eq_card_range_of_comp_eq: Nat.card (Set.range f) = Nat.card (Set.range f') when e' ∘ f = f' ∘ e with e surjective and e' injective on the range of f.

theorem Nat.card_pi_eq_prod_of_card_eq_one {ι : Type u_1} {X : ι → Type u_2} (s : Finset ι) (hX : ∀ i ∉ s, Nat.card (X i) = 1) : Nat.card ((i : ι) → X i) = ∏ i ∈ s, Nat.card (X i)

The cardinality of a product over an arbitrary index type is the product of the cardinalities of the factors over a finite set s, when every factor outside s has exactly one element.

theorem Nat.card_range_eq_card_range_of_comp_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β} {f' : γ → δ} {e : α → γ} {e' : β → δ} (he : Function.Surjective e) (he' : Set.InjOn e' (Set.range f)) (h : e' ∘ f = f' ∘ e) : Nat.card ↑(Set.range f) = Nat.card ↑(Set.range f')

Two maps f and f' with e' ∘ f = f' ∘ e, where e is surjective and e' is injective on the range of f, have ranges of the same cardinality.