theorem CategoryTheory.FiniteTensorCategoryData.absorption_identity_K0_level (D : FiniteTensorCategoryData) (fpDimZ : ℝ) (tensorDecomp : D.ι → D.ι → ℝ) (h_hom_level : ∀ (homDim : D.ι → D.ι → ℝ) (j : D.ι), ∑ i : D.ι, D.fpDimSimple i * ∑ k : D.ι, tensorDecomp i k * homDim k j = fpDimZ * ∑ i : D.ι, D.fpDimSimple i * homDim i j) (j : D.ι) : ∑ i : D.ι, D.fpDimSimple i * tensorDecomp i j = fpDimZ * D.fpDimSimple j

Extract the absorption identity at the Grothendieck-ring level from a left-Hom-level absorption hypothesis by specialising homDim to a Kronecker delta.

theorem CategoryTheory.FiniteTensorCategoryData.absorption_identity_K0_level_right (D : FiniteTensorCategoryData) (fpDimZ : ℝ) (tensorDecompRight : D.ι → D.ι → ℝ) (h_hom_level_right : ∀ (homDim : D.ι → D.ι → ℝ) (j : D.ι), ∑ i : D.ι, D.fpDimSimple i * ∑ k : D.ι, tensorDecompRight i k * homDim k j = fpDimZ * ∑ i : D.ι, D.fpDimSimple i * homDim i j) (j : D.ι) : ∑ i : D.ι, D.fpDimSimple i * tensorDecompRight i j = fpDimZ * D.fpDimSimple j

The right-handed analogue of absorption_identity_K0_level: extract the absorption identity at the Grothendieck-ring level from a right-Hom-level absorption hypothesis.

theorem CategoryTheory.FiniteTensorCategoryData.regularObject_absorption_Gr (D : FiniteTensorCategoryData) (N : D.ι → D.ι → D.ι → ℕ) (h_N : ∀ (j i : D.ι), ∑ k : D.ι, ↑(N j i k) * D.fpDimSimple k = D.fpDimSimple j * D.fpDimSimple i) (j k : D.ι) : ∑ i : D.ι, ↑(N j i k) * D.fpDimSimple i = D.fpDimSimple j * D.fpDimSimple k

Absorption identity on the Grothendieck ring: the regular object satisfies the expected eigenvalue relation with respect to the fusion coefficients.

theorem CategoryTheory.FiniteTensorCategoryData.Proposition_1_47_7_regular_absorption (D : FiniteTensorCategoryData) (N : D.ι → D.ι → D.ι → ℕ) (h_N : ∀ (j i : D.ι), ∑ k : D.ι, ↑(N j i k) * D.fpDimSimple k = D.fpDimSimple j * D.fpDimSimple i) : (∀ (fpDimZ : ℝ) (tensorDecomp : D.ι → D.ι → ℝ), (∀ (homDim : D.ι → D.ι → ℝ) (j : D.ι), ∑ i : D.ι, D.fpDimSimple i * ∑ k : D.ι, tensorDecomp i k * homDim k j = fpDimZ * ∑ i : D.ι, D.fpDimSimple i * homDim i j) → ∀ (j : D.ι), ∑ i : D.ι, D.fpDimSimple i * tensorDecomp i j = fpDimZ * D.fpDimSimple j) ∧ (∀ (fpDimZ : ℝ) (tensorDecompRight : D.ι → D.ι → ℝ), (∀ (homDim : D.ι → D.ι → ℝ) (j : D.ι), ∑ i : D.ι, D.fpDimSimple i * ∑ k : D.ι, tensorDecompRight i k * homDim k j = fpDimZ * ∑ i : D.ι, D.fpDimSimple i * homDim i j) → ∀ (j : D.ι), ∑ i : D.ι, D.fpDimSimple i * tensorDecompRight i j = fpDimZ * D.fpDimSimple j) ∧ (∀ (fpDimZ : ℝ) (tensorDecompLeft tensorDecompRight : D.ι → D.ι → ℝ), (∀ (homDim : D.ι → D.ι → ℝ) (j : D.ι), ∑ i : D.ι, D.fpDimSimple i * ∑ k : D.ι, tensorDecompLeft i k * homDim k j = fpDimZ * ∑ i : D.ι, D.fpDimSimple i * homDim i j) → (∀ (homDim : D.ι → D.ι → ℝ) (j : D.ι), ∑ i : D.ι, D.fpDimSimple i * ∑ k : D.ι, tensorDecompRight i k * homDim k j = fpDimZ * ∑ i : D.ι, D.fpDimSimple i * homDim i j) → ∀ (j : D.ι), ∑ i : D.ι, D.fpDimSimple i * tensorDecompLeft i j = ∑ i : D.ι, D.fpDimSimple i * tensorDecompRight i j) ∧ ∀ (j k : D.ι), ∑ i : D.ι, ↑(N j i k) * D.fpDimSimple i = D.fpDimSimple j * D.fpDimSimple k

Proposition 1.47.7 (Etingof–Gelaki–Nikshych–Ostrik): The regular object of a finite tensor category is absorbing for the Frobenius–Perron pairing both on the left and on the right, the two absorption identities agree, and the absorption identity holds at the Grothendieck-ring level.