Ferrers diagrams (unlabeled partitions)
module univalent-combinatorics.ferrers-diagrams where
Imports
open import foundation.cartesian-product-types open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equality-dependent-function-types open import foundation.equivalences open import foundation.fundamental-theorem-of-identity-types open import foundation.identity-types open import foundation.mere-equivalences open import foundation.propositional-truncations open import foundation.propositions open import foundation.structure-identity-principle open import foundation.subtype-identity-principle open import foundation.univalence open import foundation.universe-levels open import univalent-combinatorics.finite-types
Idea
Unlabeled partitions, also known as Ferrers diagrams, of a type A record the
number of ways in which A can be decomposed as the dependent pair type of a
family of inhabited types. More precisely, a Ferrers diagram of a type A
consists of a type X and a family Y of inhabited types over X such that
Σ X Y is merely equivalent to A. A finite Finite ferrers diagram of a finite
type A consists of a finite type X and a family Y of inhabited finite
types over X such that Σ X Y is merely equivalent to A. The number of
finite Ferrers diagrams of A is the partition number of the cardinality of
A.
Definition
Ferrers diagrams of arbitrary types
ferrers-diagram : {l1 : Level} (l2 l3 : Level) (A : UU l1) → UU (l1 ⊔ lsuc l2 ⊔ lsuc l3) ferrers-diagram l2 l3 A = Σ ( UU l2) ( λ X → Σ ( X → UU l3) ( λ Y → ((x : X) → type-trunc-Prop (Y x)) × mere-equiv A (Σ X Y))) module _ {l1 l2 l3 : Level} {A : UU l1} (D : ferrers-diagram l2 l3 A) where row-ferrers-diagram : UU l2 row-ferrers-diagram = pr1 D dot-ferrers-diagram : row-ferrers-diagram → UU l3 dot-ferrers-diagram = pr1 (pr2 D) is-inhabited-dot-ferrers-diagram : (x : row-ferrers-diagram) → type-trunc-Prop (dot-ferrers-diagram x) is-inhabited-dot-ferrers-diagram = pr1 (pr2 (pr2 D)) mere-equiv-ferrers-diagram : mere-equiv A (Σ row-ferrers-diagram dot-ferrers-diagram) mere-equiv-ferrers-diagram = pr2 (pr2 (pr2 D))
Finite Ferrers diagrams of finite types
ferrers-diagram-𝔽 : {l1 : Level} (l2 l3 : Level) (A : 𝔽 l1) → UU (l1 ⊔ lsuc l2 ⊔ lsuc l3) ferrers-diagram-𝔽 {l} l2 l3 A = Σ ( 𝔽 l2) ( λ X → Σ ( type-𝔽 X → 𝔽 l3) ( λ Y → ((x : type-𝔽 X) → type-trunc-Prop (type-𝔽 (Y x))) × mere-equiv (type-𝔽 A) (Σ (type-𝔽 X) (λ x → type-𝔽 (Y x))))) module _ {l1 l2 l3 : Level} (A : 𝔽 l1) (D : ferrers-diagram-𝔽 l2 l3 A) where row-ferrers-diagram-𝔽 : 𝔽 l2 row-ferrers-diagram-𝔽 = pr1 D type-row-ferrers-diagram-𝔽 : UU l2 type-row-ferrers-diagram-𝔽 = type-𝔽 row-ferrers-diagram-𝔽 is-finite-type-row-ferrers-diagram-𝔽 : is-finite type-row-ferrers-diagram-𝔽 is-finite-type-row-ferrers-diagram-𝔽 = is-finite-type-𝔽 row-ferrers-diagram-𝔽 dot-ferrers-diagram-𝔽 : type-row-ferrers-diagram-𝔽 → 𝔽 l3 dot-ferrers-diagram-𝔽 = pr1 (pr2 D) type-dot-ferrers-diagram-𝔽 : type-row-ferrers-diagram-𝔽 → UU l3 type-dot-ferrers-diagram-𝔽 x = type-𝔽 (dot-ferrers-diagram-𝔽 x) is-finite-type-dot-ferrers-diagram-𝔽 : (x : type-row-ferrers-diagram-𝔽) → is-finite (type-dot-ferrers-diagram-𝔽 x) is-finite-type-dot-ferrers-diagram-𝔽 x = is-finite-type-𝔽 (dot-ferrers-diagram-𝔽 x) is-inhabited-dot-ferrers-diagram-𝔽 : (x : type-row-ferrers-diagram-𝔽) → type-trunc-Prop (type-dot-ferrers-diagram-𝔽 x) is-inhabited-dot-ferrers-diagram-𝔽 = pr1 (pr2 (pr2 D)) mere-equiv-ferrers-diagram-𝔽 : mere-equiv ( type-𝔽 A) ( Σ (type-row-ferrers-diagram-𝔽) (type-dot-ferrers-diagram-𝔽)) mere-equiv-ferrers-diagram-𝔽 = pr2 (pr2 (pr2 D)) ferrers-diagram-ferrers-diagram-𝔽 : ferrers-diagram l2 l3 (type-𝔽 A) pr1 ferrers-diagram-ferrers-diagram-𝔽 = type-row-ferrers-diagram-𝔽 pr1 (pr2 ferrers-diagram-ferrers-diagram-𝔽) = type-dot-ferrers-diagram-𝔽 pr1 (pr2 (pr2 ferrers-diagram-ferrers-diagram-𝔽)) = is-inhabited-dot-ferrers-diagram-𝔽 pr2 (pr2 (pr2 ferrers-diagram-ferrers-diagram-𝔽)) = mere-equiv-ferrers-diagram-𝔽
Equivalences of Ferrers diagrams
module _ {l1 l2 l3 : Level} {A : UU l1} (D : ferrers-diagram l2 l3 A) where equiv-ferrers-diagram : {l4 l5 : Level} (E : ferrers-diagram l4 l5 A) → UU (l2 ⊔ l3 ⊔ l4 ⊔ l5) equiv-ferrers-diagram E = Σ ( row-ferrers-diagram D ≃ row-ferrers-diagram E) ( λ e → (x : row-ferrers-diagram D) → dot-ferrers-diagram D x ≃ dot-ferrers-diagram E (map-equiv e x)) id-equiv-ferrers-diagram : equiv-ferrers-diagram D pr1 id-equiv-ferrers-diagram = id-equiv pr2 id-equiv-ferrers-diagram x = id-equiv equiv-eq-ferrers-diagram : (E : ferrers-diagram l2 l3 A) → Id D E → equiv-ferrers-diagram E equiv-eq-ferrers-diagram .D refl = id-equiv-ferrers-diagram is-contr-total-equiv-ferrers-diagram : is-contr (Σ (ferrers-diagram l2 l3 A) (equiv-ferrers-diagram)) is-contr-total-equiv-ferrers-diagram = is-contr-total-Eq-structure ( λ X Y e → (x : row-ferrers-diagram D) → dot-ferrers-diagram D x ≃ pr1 Y (map-equiv e x)) ( is-contr-total-equiv (row-ferrers-diagram D)) ( pair (row-ferrers-diagram D) id-equiv) ( is-contr-total-Eq-subtype ( is-contr-total-equiv-fam (dot-ferrers-diagram D)) ( λ Y → is-prop-prod ( is-prop-Π (λ x → is-prop-type-trunc-Prop)) ( is-prop-mere-equiv A (Σ (row-ferrers-diagram D) Y))) ( dot-ferrers-diagram D) ( λ x → id-equiv) ( pair ( is-inhabited-dot-ferrers-diagram D) ( mere-equiv-ferrers-diagram D))) is-equiv-equiv-eq-ferrers-diagram : (E : ferrers-diagram l2 l3 A) → is-equiv (equiv-eq-ferrers-diagram E) is-equiv-equiv-eq-ferrers-diagram = fundamental-theorem-id is-contr-total-equiv-ferrers-diagram equiv-eq-ferrers-diagram eq-equiv-ferrers-diagram : (E : ferrers-diagram l2 l3 A) → equiv-ferrers-diagram E → Id D E eq-equiv-ferrers-diagram E = map-inv-is-equiv (is-equiv-equiv-eq-ferrers-diagram E)
Equivalences of finite ferrers diagrams of finite types
module _ {l1 l2 l3 : Level} (A : 𝔽 l1) (D : ferrers-diagram-𝔽 l2 l3 A) where equiv-ferrers-diagram-𝔽 : {l4 l5 : Level} → ferrers-diagram-𝔽 l4 l5 A → UU (l2 ⊔ l3 ⊔ l4 ⊔ l5) equiv-ferrers-diagram-𝔽 E = equiv-ferrers-diagram ( ferrers-diagram-ferrers-diagram-𝔽 A D) ( ferrers-diagram-ferrers-diagram-𝔽 A E) id-equiv-ferrers-diagram-𝔽 : equiv-ferrers-diagram-𝔽 D id-equiv-ferrers-diagram-𝔽 = id-equiv-ferrers-diagram (ferrers-diagram-ferrers-diagram-𝔽 A D) equiv-eq-ferrers-diagram-𝔽 : (E : ferrers-diagram-𝔽 l2 l3 A) → Id D E → equiv-ferrers-diagram-𝔽 E equiv-eq-ferrers-diagram-𝔽 .D refl = id-equiv-ferrers-diagram-𝔽 is-contr-total-equiv-ferrers-diagram-𝔽 : is-contr (Σ (ferrers-diagram-𝔽 l2 l3 A) (equiv-ferrers-diagram-𝔽)) is-contr-total-equiv-ferrers-diagram-𝔽 = is-contr-total-Eq-structure ( λ X Y e → (x : type-row-ferrers-diagram-𝔽 A D) → type-dot-ferrers-diagram-𝔽 A D x ≃ type-𝔽 (pr1 Y (map-equiv e x))) ( is-contr-total-Eq-subtype ( is-contr-total-equiv (type-row-ferrers-diagram-𝔽 A D)) ( is-prop-is-finite) ( type-row-ferrers-diagram-𝔽 A D) ( id-equiv) ( is-finite-type-row-ferrers-diagram-𝔽 A D)) ( pair (row-ferrers-diagram-𝔽 A D) id-equiv) ( is-contr-total-Eq-subtype ( is-contr-total-Eq-Π ( λ x Y → type-dot-ferrers-diagram-𝔽 A D x ≃ type-𝔽 Y) ( λ x → is-contr-total-Eq-subtype ( is-contr-total-equiv (type-dot-ferrers-diagram-𝔽 A D x)) ( is-prop-is-finite) ( type-dot-ferrers-diagram-𝔽 A D x) ( id-equiv) ( is-finite-type-dot-ferrers-diagram-𝔽 A D x))) ( λ x → is-prop-prod ( is-prop-Π (λ x → is-prop-type-trunc-Prop)) ( is-prop-mere-equiv (type-𝔽 A) _)) ( dot-ferrers-diagram-𝔽 A D) ( λ x → id-equiv) ( pair ( is-inhabited-dot-ferrers-diagram-𝔽 A D) ( mere-equiv-ferrers-diagram-𝔽 A D))) is-equiv-equiv-eq-ferrers-diagram-𝔽 : (E : ferrers-diagram-𝔽 l2 l3 A) → is-equiv (equiv-eq-ferrers-diagram-𝔽 E) is-equiv-equiv-eq-ferrers-diagram-𝔽 = fundamental-theorem-id is-contr-total-equiv-ferrers-diagram-𝔽 equiv-eq-ferrers-diagram-𝔽 eq-equiv-ferrers-diagram-𝔽 : (E : ferrers-diagram-𝔽 l2 l3 A) → equiv-ferrers-diagram-𝔽 E → Id D E eq-equiv-ferrers-diagram-𝔽 E = map-inv-is-equiv (is-equiv-equiv-eq-ferrers-diagram-𝔽 E)
Properties
The type of Ferrers diagrams of any finite type is π-finite
This remains to be shown.
See also
- Integer partitions in
elementary-number-theory.integer-partitions