The numerical profile of one Drozd--Kiričenko rejection #
Removing a non-simple indecomposable projective-injective deletes one projective vertex of incoming arity one. Its unique successor becomes projective and loses the deleted vertex from its incoming middle term; all other projectivity predicates and incoming arities are unchanged. This file packages exactly that finite-tau profile and proves that it preserves the Auslander--Reiten surplus.
structure
MagnitudeConjecture.FiniteTauMatrix.RejectionProfile
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
(ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I)
(rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J)
:
Type (max w₁ w₂)
The exact finite-tau change caused by rejecting one non-simple
indecomposable projective-injective. ambient is the category before
rejection and rejected is the category afterwards.
- deleted : I
The removed projective-injective label.
- replacement : J
The surviving label represented by
U / soc(U), which becomes projective after rejection. - surviving : J ≃ { i : I // i ≠ self.deleted }
The rejected labels are exactly the ambient labels other than the deleted one.
- deleted_projective : ambient.IsProjective self.deleted
- deleted_arity : rightMiddleArity ambient self.deleted = 1
- replacement_ambient_nonprojective : ¬ambient.IsProjective ↑(self.surviving self.replacement)
- replacement_rejected_projective : rejected.IsProjective self.replacement
- projective_iff_of_ne (j : J) : j ≠ self.replacement → (ambient.IsProjective ↑(self.surviving j) ↔ rejected.IsProjective j)
- replacement_arity : rightMiddleArity rejected self.replacement + 1 = rightMiddleArity ambient ↑(self.surviving self.replacement)
- arity_eq_of_ne (j : J) : j ≠ self.replacement → rightMiddleArity ambient ↑(self.surviving j) = rightMiddleArity rejected j
Instances For
@[instance_reducible]
noncomputable def
MagnitudeConjecture.FiniteTauMatrix.RejectionProfile.rejectionProfileAmbientProjectiveDecidable
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{I : Type w₁}
[Fintype I]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
:
DecidablePred ambient.IsProjective
Instances For
@[instance_reducible]
noncomputable def
MagnitudeConjecture.FiniteTauMatrix.RejectionProfile.rejectionProfileRejectedProjectiveDecidable
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{J : Type w₂}
[Fintype J]
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
:
DecidablePred rejected.IsProjective
Instances For
@[instance_reducible]
noncomputable def
MagnitudeConjecture.FiniteTauMatrix.RejectionProfile.rejectionProfileDecidableEqI
{I : Type w₁}
:
DecidableEq I
Instances For
@[instance_reducible]
noncomputable def
MagnitudeConjecture.FiniteTauMatrix.RejectionProfile.rejectionProfileDecidableEqJ
{J : Type w₂}
:
DecidableEq J
Instances For
theorem
MagnitudeConjecture.FiniteTauMatrix.RejectionProfile.localDensity_deleted
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
(R : RejectionProfile ambient rejected)
:
ARCount.localDensity (arrowMultiplicity ambient) ambient.IsProjective R.deleted = -1
The removed projective vertex contributes local density -1.
theorem
MagnitudeConjecture.FiniteTauMatrix.RejectionProfile.localDensity_surviving_replacement
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
(R : RejectionProfile ambient rejected)
:
ARCount.localDensity (arrowMultiplicity ambient) ambient.IsProjective ↑(R.surviving R.replacement) = ARCount.localDensity (arrowMultiplicity rejected) rejected.IsProjective R.replacement + 1
The replacement vertex gains one unit of local density: it becomes projective while losing one incoming occurrence.
theorem
MagnitudeConjecture.FiniteTauMatrix.RejectionProfile.localDensity_surviving_of_ne
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
(R : RejectionProfile ambient rejected)
(j : J)
(hj : j ≠ R.replacement)
:
ARCount.localDensity (arrowMultiplicity ambient) ambient.IsProjective ↑(R.surviving j) = ARCount.localDensity (arrowMultiplicity rejected) rejected.IsProjective j
Every other surviving vertex has unchanged local density.
theorem
MagnitudeConjecture.FiniteTauMatrix.RejectionProfile.localDensity_surviving
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
(R : RejectionProfile ambient rejected)
(j : J)
:
ARCount.localDensity (arrowMultiplicity ambient) ambient.IsProjective ↑(R.surviving j) = ARCount.localDensity (arrowMultiplicity rejected) rejected.IsProjective j + if j = R.replacement then 1 else 0
Uniform indicator form of the local-density change on surviving vertices.
theorem
MagnitudeConjecture.FiniteTauMatrix.RejectionProfile.projectiveIndicator_surviving
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
(R : RejectionProfile ambient rejected)
(j : J)
:
((if ambient.IsProjective ↑(R.surviving j) then 1 else 0) + if j = R.replacement then 1 else 0) = if rejected.IsProjective j then 1 else 0
The projective indicator on surviving vertices gains exactly the replacement vertex.
theorem
MagnitudeConjecture.FiniteTauMatrix.RejectionProfile.projectiveCount_eq
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
(R : RejectionProfile ambient rejected)
:
ARCount.projectiveCount ambient.IsProjective = ARCount.projectiveCount rejected.IsProjective
One rejection replaces the deleted projective by the newly projective successor, so the number of projective vertices is unchanged.
theorem
MagnitudeConjecture.FiniteTauMatrix.RejectionProfile.vertexCount_eq_add_one
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
(R : RejectionProfile ambient rejected)
:
The rejected category has exactly one fewer indecomposable label.
theorem
MagnitudeConjecture.FiniteTauMatrix.RejectionProfile.meshCount_eq_add_one
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
(R : RejectionProfile ambient rejected)
:
ARCount.meshCount ambient.IsProjective = ARCount.meshCount rejected.IsProjective + 1
Exactly one almost-split mesh disappears under one rejection.
theorem
MagnitudeConjecture.FiniteTauMatrix.RejectionProfile.surplus_eq
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
(R : RejectionProfile ambient rejected)
:
ARCount.surplus (arrowMultiplicity ambient) ambient.IsProjective = ARCount.surplus (arrowMultiplicity rejected) rejected.IsProjective
One Drozd--Kiričenko rejection preserves the total Auslander--Reiten surplus.
theorem
MagnitudeConjecture.FiniteTauMatrix.RejectionProfile.arrowCount_eq_add_two
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
(R : RejectionProfile ambient rejected)
:
ARCount.arrowCount (arrowMultiplicity ambient) = ARCount.arrowCount (arrowMultiplicity rejected) + 2
Exactly two Auslander--Reiten arrows disappear under one rejection.
theorem
MagnitudeConjecture.FiniteTauMatrix.RejectionProfile.eulerMagnitude_eq
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
(R : RejectionProfile ambient rejected)
:
ARCount.eulerMagnitude (arrowMultiplicity ambient) ambient.IsProjective = ARCount.eulerMagnitude (arrowMultiplicity rejected) rejected.IsProjective
Consequently one rejection preserves the Auslander--Reiten Euler magnitude, not merely its surplus.
structure
MagnitudeConjecture.FiniteTauMatrix.FamilyRejectionProfile
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
(ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I)
(rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J)
:
Type (max w₁ w₂)
The exact finite-tau change caused by simultaneously rejecting a finite basic family of non-simple indecomposable projective-injectives.
- deleted : Finset I
The removed projective-injective labels.
- replacement : ↥self.deleted → J
Each deleted label has its own surviving replacement.
- replacement_injective : Function.Injective self.replacement
- surviving : J ≃ { i : I // i ∉ self.deleted }
The rejected labels are exactly the complement of the deleted family.
- replacement_ambient_nonprojective (d : ↥self.deleted) : ¬ambient.IsProjective ↑(self.surviving (self.replacement d))
- replacement_rejected_projective (d : ↥self.deleted) : rejected.IsProjective (self.replacement d)
- projective_iff_of_not_replacement (j : J) : (∀ (d : ↥self.deleted), self.replacement d ≠ j) → (ambient.IsProjective ↑(self.surviving j) ↔ rejected.IsProjective j)
- replacement_arity (d : ↥self.deleted) : rightMiddleArity rejected (self.replacement d) + 1 = rightMiddleArity ambient ↑(self.surviving (self.replacement d))
- arity_eq_of_not_replacement (j : J) : (∀ (d : ↥self.deleted), self.replacement d ≠ j) → rightMiddleArity ambient ↑(self.surviving j) = rightMiddleArity rejected j
Instances For
@[instance_reducible]
noncomputable def
MagnitudeConjecture.FiniteTauMatrix.FamilyRejectionProfile.familyRejectionProfileAmbientProjectiveDecidable
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{I : Type w₁}
[Fintype I]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
:
DecidablePred ambient.IsProjective
Instances For
@[instance_reducible]
noncomputable def
MagnitudeConjecture.FiniteTauMatrix.FamilyRejectionProfile.familyRejectionProfileRejectedProjectiveDecidable
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{J : Type w₂}
[Fintype J]
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
:
DecidablePred rejected.IsProjective
Instances For
@[instance_reducible]
noncomputable def
MagnitudeConjecture.FiniteTauMatrix.FamilyRejectionProfile.familyRejectionProfileDecidableEqI
{I : Type w₁}
:
DecidableEq I
Instances For
@[instance_reducible]
noncomputable def
MagnitudeConjecture.FiniteTauMatrix.FamilyRejectionProfile.familyRejectionProfileDecidableEqJ
{J : Type w₂}
:
DecidableEq J
Instances For
theorem
MagnitudeConjecture.FiniteTauMatrix.FamilyRejectionProfile.localDensity_deleted
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
(R : FamilyRejectionProfile ambient rejected)
(i : I)
(hi : i ∈ R.deleted)
:
ARCount.localDensity (arrowMultiplicity ambient) ambient.IsProjective i = -1
Every deleted projective vertex contributes local density -1.
theorem
MagnitudeConjecture.FiniteTauMatrix.FamilyRejectionProfile.localDensity_surviving_replacement
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
(R : FamilyRejectionProfile ambient rejected)
(d : ↥R.deleted)
:
ARCount.localDensity (arrowMultiplicity ambient) ambient.IsProjective ↑(R.surviving (R.replacement d)) = ARCount.localDensity (arrowMultiplicity rejected) rejected.IsProjective (R.replacement d) + 1
Every replacement gains one unit of local density.
theorem
MagnitudeConjecture.FiniteTauMatrix.FamilyRejectionProfile.localDensity_surviving_of_not_replacement
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
(R : FamilyRejectionProfile ambient rejected)
(j : J)
(hj : ∀ (d : ↥R.deleted), R.replacement d ≠ j)
:
ARCount.localDensity (arrowMultiplicity ambient) ambient.IsProjective ↑(R.surviving j) = ARCount.localDensity (arrowMultiplicity rejected) rejected.IsProjective j
Every surviving vertex outside the replacement family has unchanged local density.
theorem
MagnitudeConjecture.FiniteTauMatrix.FamilyRejectionProfile.localDensity_surviving
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
(R : FamilyRejectionProfile ambient rejected)
(j : J)
:
ARCount.localDensity (arrowMultiplicity ambient) ambient.IsProjective ↑(R.surviving j) = ARCount.localDensity (arrowMultiplicity rejected) rejected.IsProjective j + if ∃ (d : ↥R.deleted), R.replacement d = j then 1 else 0
Uniform indicator form of the local-density change on surviving vertices.
theorem
MagnitudeConjecture.FiniteTauMatrix.FamilyRejectionProfile.projectiveIndicator_surviving
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
(R : FamilyRejectionProfile ambient rejected)
(j : J)
:
((if ambient.IsProjective ↑(R.surviving j) then 1 else 0) + if ∃ (d : ↥R.deleted), R.replacement d = j then 1 else 0) = if rejected.IsProjective j then 1 else 0
Uniform projective-indicator change on surviving vertices.
theorem
MagnitudeConjecture.FiniteTauMatrix.FamilyRejectionProfile.sum_replacementIndicator
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
(R : FamilyRejectionProfile ambient rejected)
:
(∑ j : J, if ∃ (d : ↥R.deleted), R.replacement d = j then 1 else 0) = ↑R.deleted.card
The sum of replacement indicators is the size of the deleted family.
theorem
MagnitudeConjecture.FiniteTauMatrix.FamilyRejectionProfile.projectiveCount_eq
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
(R : FamilyRejectionProfile ambient rejected)
:
ARCount.projectiveCount ambient.IsProjective = ARCount.projectiveCount rejected.IsProjective
Simultaneous rejection replaces all deleted projectives by the same number of new projective replacement vertices.
theorem
MagnitudeConjecture.FiniteTauMatrix.FamilyRejectionProfile.surplus_eq
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
(R : FamilyRejectionProfile ambient rejected)
:
ARCount.surplus (arrowMultiplicity ambient) ambient.IsProjective = ARCount.surplus (arrowMultiplicity rejected) rejected.IsProjective
Simultaneous rejection preserves the total Auslander--Reiten surplus.
theorem
MagnitudeConjecture.FiniteTauMatrix.FamilyRejectionProfile.eulerMagnitude_eq
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
{ambient : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I}
{rejected : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J}
(R : FamilyRejectionProfile ambient rejected)
:
ARCount.eulerMagnitude (arrowMultiplicity ambient) ambient.IsProjective = ARCount.eulerMagnitude (arrowMultiplicity rejected) rejected.IsProjective
A simultaneous finite family rejection preserves the Auslander--Reiten Euler magnitude.