Intrinsic irreducible spaces under linear equivalences

theorem MagnitudeConjecture.radical_comap_equivalence {C : Type u} {D : Type v} [CategoryTheory.Category.{w, u} C] [CategoryTheory.Category.{w, v} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (E : C ≌ D) [E.functor.Additive] : QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.comap E.functor QuotientSubmoduleEquidistribution.CategoricalRadical.homIdeal = QuotientSubmoduleEquidistribution.CategoricalRadical.homIdeal

Equivalences preserve and reflect the intrinsic radical ideal.

theorem MagnitudeConjecture.radicalSquare_map_equivalence_iff {C : Type u} {D : Type v} [CategoryTheory.Category.{w, u} C] [CategoryTheory.Category.{w, v} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (E : C ≌ D) [E.functor.Additive] {X Y : C} (f : X ⟶ Y) : E.functor.map f ∈ (QuotientSubmoduleEquidistribution.CategoricalRadical.homIdeal ⋆ᵢ QuotientSubmoduleEquidistribution.CategoricalRadical.homIdeal).hom (E.functor.obj X) (E.functor.obj Y) ↔ f ∈ (QuotientSubmoduleEquidistribution.CategoricalRadical.homIdeal ⋆ᵢ QuotientSubmoduleEquidistribution.CategoricalRadical.homIdeal).hom X Y

Radical-square membership is invariant under equivalence.

noncomputable def MagnitudeConjecture.CategoricalIrreducible.radicalEquivalence {C : Type u} {D : Type v} [CategoryTheory.Category.{w, u} C] [CategoryTheory.Category.{w, v} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (k : Type z) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (E : C ≌ D) [E.functor.Additive] [CategoryTheory.Functor.Linear k E.functor] (X Y : C) : ↥(radical k X Y) ≃ₗ[k] ↥(radical k (E.functor.obj X) (E.functor.obj Y))

Restrict the Hom map of a linear equivalence to radical numerators.

theorem MagnitudeConjecture.CategoricalIrreducible.denominator_map_equivalence {C : Type u} {D : Type v} [CategoryTheory.Category.{w, u} C] [CategoryTheory.Category.{w, v} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (k : Type z) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (E : C ≌ D) [E.functor.Additive] [CategoryTheory.Functor.Linear k E.functor] (X Y : C) : Submodule.map (↑(radicalEquivalence k E X Y)) (denominator k X Y) = denominator k (E.functor.obj X) (E.functor.obj Y)

The radical numerator equivalence carries the radical-square denominator onto the corresponding denominator.

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

A linear category equivalence induces a linear equivalence on intrinsic irreducible quotients.