Magnitude conjecture

MagnitudeConjecture.CategoryTheory.IrreducibleSpaceIso

Intrinsic irreducible quotients under changes of representatives #

source
theorem MagnitudeConjecture.homIdeal_mem_iso_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal C) {X X' Y Y' : C} (i : X ≅ X') (j : Y ≅ Y') (f : X ⟶ Y) :
CategoryTheory.CategoryStruct.comp i.inv (CategoryTheory.CategoryStruct.comp f j.hom) ∈ I.hom X' Y' ↔ f ∈ I.hom X Y

Membership in any Hom ideal is invariant under conjugating its endpoints by isomorphisms.

source
def MagnitudeConjecture.CategoricalIrreducible.radicalIsoEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type w) [Field k] [CategoryTheory.Linear k C] {X X' Y Y' : C} (i : X ≅ X') (j : Y ≅ Y') :
↥(radical k X Y) ≃ₗ[k] ↥(radical k X' Y')

Changing representatives induces a linear equivalence on radical numerators.

Instances For
    source
    theorem MagnitudeConjecture.CategoricalIrreducible.denominator_map_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type w) [Field k] [CategoryTheory.Linear k C] {X X' Y Y' : C} (i : X ≅ X') (j : Y ≅ Y') :
    Submodule.map (↑(radicalIsoEquiv k i j)) (denominator k X Y) = denominator k X' Y'

    The change of representatives identifies the radical-square denominators.

    source
    def MagnitudeConjecture.CategoricalIrreducible.spaceIsoEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type w) [Field k] [CategoryTheory.Linear k C] {X X' Y Y' : C} (i : X ≅ X') (j : Y ≅ Y') :
    Space k X Y ≃ₗ[k] Space k X' Y'

    Intrinsic irreducible quotient spaces do not depend on the chosen representatives.

    Instances For
      source
      noncomputable def MagnitudeConjecture.CategoricalIrreducible.spaceInverseEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type w) [Field k] [CategoryTheory.Linear k C] {D : Type u_1} [CategoryTheory.Category.{v, u_1} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (E : C ≌ D) [E.functor.Additive] [CategoryTheory.Functor.Linear k E.functor] (X Y : D) :
      Space k (E.inverse.obj X) (E.inverse.obj Y) ≃ₗ[k] Space k X Y

      The inverse realization identifies quotient spaces with the original objects, using the counit to remove the change of representatives.

      Instances For