Documentation

Atlas.AlgebraicCombinatorics.code.YoungLattice

Definition of L(m,n) #

source
def YoungLattice.Lmn (m n : ℕ) :
Type

Lmn m n is the poset of partitions fitting in an m × n rectangle, modeled as antitone functions Fin m → Fin (n+1). The value f(i) represents the i-th part of the partition (weakly decreasing).

Instances For

    Basic instances #

    source
    @[implicit_reducible]
    instance YoungLattice.Lmn.instPartialOrder (m n : ℕ) :
    PartialOrder (Lmn m n)
    source
    @[implicit_reducible]
    noncomputable instance YoungLattice.Lmn.instDecidableEq (m n : ℕ) :
    DecidableEq (Lmn m n)
    source
    @[implicit_reducible]
    noncomputable instance YoungLattice.Lmn.instFintype (m n : ℕ) :
    Fintype (Lmn m n)
    source
    theorem YoungLattice.Lmn.ext {m n : ℕ} {p q : Lmn m n} (h : ∀ (i : Fin m), ↑p i = ↑q i) :
    p = q
    source
    theorem YoungLattice.Lmn.ext_iff {m n : ℕ} {p q : Lmn m n} :
    p = q ↔ ∀ (i : Fin m), ↑p i = ↑q i

    Sum of parts (rank function) #

    source
    def YoungLattice.Lmn.sumParts {m n : ℕ} (p : Lmn m n) :
    ℕ

    The rank of a partition is the sum of its parts.

    Instances For

      Zero and top elements #

      source
      def YoungLattice.Lmn.zero (m n : ℕ) :
      Lmn m n

      The zero partition (all parts 0).

      Instances For
        source
        def YoungLattice.Lmn.top (m n : ℕ) :
        Lmn m n

        The maximal partition (all parts equal to n).

        Instances For
          source
          theorem YoungLattice.Lmn.zero_le {m n : ℕ} (p : Lmn m n) :
          zero m n ≤ p
          source
          theorem YoungLattice.Lmn.le_top {m n : ℕ} (p : Lmn m n) :
          p ≤ top m n
          source
          theorem YoungLattice.Lmn.sumParts_zero {m n : ℕ} :
          (zero m n).sumParts = 0
          source
          theorem YoungLattice.Lmn.sumParts_top {m n : ℕ} :
          (top m n).sumParts = m * n

          IsMin characterization #

          source
          theorem YoungLattice.Lmn.isMin_iff {m n : ℕ} {p : Lmn m n} :
          IsMin p ↔ p = zero m n

          Strict monotonicity of sumParts #

          source
          theorem YoungLattice.Lmn.sumParts_strictMono {m n : ℕ} :
          StrictMono sumParts

          CovBy property #

          source
          theorem YoungLattice.Lmn.exists_between {m n : ℕ} {p q : Lmn m n} (hle : ∀ (i : Fin m), ↑p i ≤ ↑q i) (hne : p ≠ q) (hge2 : q.sumParts ≥ p.sumParts + 2) :
          ∃ (r : Lmn m n), p ≤ r ∧ r < q ∧ p ≠ r

          If p < q in Lmn with sum difference ≥ 2, there exists an intermediate element.

          source
          theorem YoungLattice.Lmn.covBy_sumParts {m n : ℕ} {p q : Lmn m n} (h : p ⋖ q) :
          p.sumParts ⋖ q.sumParts

          If p ⋖ q in Lmn, then sumParts p ⋖ sumParts q in ℕ.

          source
          theorem YoungLattice.Lmn.isMin_sumParts {m n : ℕ} {p : Lmn m n} (h : IsMin p) :
          IsMin p.sumParts

          Minimal elements have sumParts = 0.

          GradeOrder and GradeMinOrder instances #

          source
          @[implicit_reducible]
          instance YoungLattice.Lmn.instGradeOrder (m n : ℕ) :
          GradeOrder ℕ (Lmn m n)
          source
          @[implicit_reducible]
          instance YoungLattice.Lmn.instGradeMinOrder (m n : ℕ) :
          GradeMinOrder ℕ (Lmn m n)
          source
          theorem YoungLattice.Lmn.grade_eq {m n : ℕ} (p : Lmn m n) :
          grade ℕ p = p.sumParts

          Complement operation #

          source
          def YoungLattice.Lmn.complement {m n : ℕ} (p : Lmn m n) :
          Lmn m n

          The complement of a partition λ in the m×n rectangle: rotate the complement of λ's Young diagram by 180°. In coordinates: λ̃_i = n - λ_{m+1-i}.

          Instances For
            source
            theorem YoungLattice.Lmn.complement_complement {m n : ℕ} (p : Lmn m n) :
            p.complement.complement = p

            Complementing twice gives back the original partition.

            source
            theorem YoungLattice.Lmn.complement_injective {m n : ℕ} :
            Function.Injective complement

            The complement is injective.

            source
            theorem YoungLattice.Lmn.sumParts_complement_add {m n : ℕ} (p : Lmn m n) :
            p.complement.sumParts + p.sumParts = m * n

            Sum of parts of complement + sum of parts = m * n.

            source
            theorem YoungLattice.Lmn.grade_complement {m n : ℕ} (p : Lmn m n) :
            grade ℕ p.complement = m * n - grade ℕ p

            The grade of the complement equals m*n minus the grade.

            GradedPoset instance #

            source
            theorem YoungLattice.Lmn.grade_le_mul {m n : ℕ} (p : Lmn m n) :
            grade ℕ p ≤ m * n
            source
            @[implicit_reducible]
            instance YoungLattice.Lmn.instGradedPoset (m n : ℕ) :
            SpernerProperty.GradedPoset (Lmn m n)

            Rank-symmetry #

            source
            theorem YoungLattice.Lmn.Lmn_isRankSymmetric (m n : ℕ) :
            SpernerProperty.IsRankSymmetric

            L(m,n) is rank-symmetric: the complement operation gives a bijection between elements of rank i and elements of rank mn - i.

            Rank-unimodality (Corollary 6.10) #

            L(m,n) is rank-unimodal. The proof is in YoungLatticeSperner.lean, which can import both QuotientIsoLmn and GroupActions without circular dependencies. See YoungLattice.Lmn.Lmn_isRankUnimodal.

            Sperner property (Corollary 6.10) #

            L(m,n) has the Sperner property. The proof is in YoungLatticeSperner.lean, which can import both QuotientIsoLmn and GroupActions without circular dependencies. See YoungLattice.Lmn.hasSpernerProperty.