Magnitude conjecture

MagnitudeConjecture.Algebra.RightModulePrimitiveArrowDescent

Irreducible-arrow descent under primitive deletion #

Inflation identifies the Hom and radical spaces between two modules over A / AeA with their ambient counterparts. A quotient radical-square factorization is still a radical-square factorization after inflation, while the ambient category may have additional intermediate modules. Consequently there is a canonical surjection Irr_(A/AeA)(X,Y) ⟶ Irr_A(X,Y), giving the arrow-multiplicity inequality used in the live manuscript.

source
@[instance_reducible]
noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveArrowDescentQuotientFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) :
Fintype (S.PrimitiveQuotientLabel D)
Instances For
    source
    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientInflationFunctor {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} :
    CategoryTheory.Functor (FinitelyGeneratedCategory (primitiveQuotientAlgebra e)) (FinitelyGeneratedCategory A)

    Inflation from the primitive quotient to ambient finitely generated right modules.

    Instances For
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientInflationFunctorAdditive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} :
      primitiveQuotientInflationFunctor.Additive
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientInflationFunctorLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} :
      CategoryTheory.Functor.Linear k primitiveQuotientInflationFunctor
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientInflationFunctorFull {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} :
      primitiveQuotientInflationFunctor.Full
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientInflationFunctorFaithful {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} :
      primitiveQuotientInflationFunctor.Faithful
      source
      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientInflationObjIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (x : S.PrimitiveQuotientLabel D) :
      primitiveQuotientInflationFunctor.obj (S.primitiveQuotientFGObj D x) ≅ S.fgObj ↑x

      Inflation of a literal quotient representative recovers its ambient representative.

      Instances For
        source
        noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientHomAmbientLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (x y : S.PrimitiveQuotientLabel D) :
        (S.primitiveQuotientFGObj D x ⟶ S.primitiveQuotientFGObj D y) ≃ₗ[k] S.fgObj ↑x ⟶ S.fgObj ↑y

        Inflation and the endpoint identifications give the common Hom space between two surviving indecomposables.

        Instances For
          source
          @[simp]
          theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientHomAmbientLinearEquiv_apply {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (x y : S.PrimitiveQuotientLabel D) (f : S.primitiveQuotientFGObj D x ⟶ S.primitiveQuotientFGObj D y) :
          (S.primitiveQuotientHomAmbientLinearEquiv D x y) f = CategoryTheory.CategoryStruct.comp (S.primitiveQuotientInflationObjIso D x).inv (CategoryTheory.CategoryStruct.comp (primitiveQuotientInflationFunctor.map f) (S.primitiveQuotientInflationObjIso D y).hom)
          source
          noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientLinearMapAmbientLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (x y : S.PrimitiveQuotientLabel D) :
          (↑(S.primitiveQuotientFGObj D x) →ₗ[(primitiveQuotientAlgebra e)ᵐᵒᵖ] ↑(S.primitiveQuotientFGObj D y)) ≃ₗ[k] ↑(S.fgObj ↑x) →ₗ[Aᵐᵒᵖ] ↑(S.fgObj ↑y)

          The common Hom-space identification at the level of underlying linear maps used by the irreducible-Hom API.

          Instances For
            source
            @[simp]
            theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientLinearMapAmbientLinearEquiv_ofHom {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (x y : S.PrimitiveQuotientLabel D) (f : ↑(S.primitiveQuotientFGObj D x) →ₗ[(primitiveQuotientAlgebra e)ᵐᵒᵖ] ↑(S.primitiveQuotientFGObj D y)) :
            CategoryTheory.ConcreteCategory.ofHom ((S.primitiveQuotientLinearMapAmbientLinearEquiv D x y) f) = (S.primitiveQuotientHomAmbientLinearEquiv D x y) (CategoryTheory.ConcreteCategory.ofHom f)
            source
            theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientHomAmbientLinearEquiv_isSplitEpi_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (x y : S.PrimitiveQuotientLabel D) (f : S.primitiveQuotientFGObj D x ⟶ S.primitiveQuotientFGObj D y) :
            CategoryTheory.IsSplitEpi ((S.primitiveQuotientHomAmbientLinearEquiv D x y) f) ↔ CategoryTheory.IsSplitEpi f

            Inflation preserves and reflects split epimorphisms between the fixed surviving representatives.

            source
            theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientLinearMapAmbientLinearEquiv_isSplitEpi_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (x y : S.PrimitiveQuotientLabel D) (f : ↑(S.primitiveQuotientFGObj D x) →ₗ[(primitiveQuotientAlgebra e)ᵐᵒᵖ] ↑(S.primitiveQuotientFGObj D y)) :
            CategoryTheory.IsSplitEpi (CategoryTheory.ConcreteCategory.ofHom ((S.primitiveQuotientLinearMapAmbientLinearEquiv D x y) f)) ↔ CategoryTheory.IsSplitEpi (CategoryTheory.ConcreteCategory.ofHom f)

            The underlying common-Hom equivalence preserves and reflects split epimorphisms.

            source
            @[instance_reducible]
            noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveArrowDescentAmbientModule {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) :
            Module k ↑(S.almostSplitSkeleton.obj i)
            Instances For
              source
              theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveArrowDescentAmbientTower {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) :
              IsScalarTower k Aᵐᵒᵖ ↑(S.almostSplitSkeleton.obj i)
              source
              @[instance_reducible]
              noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveArrowDescentQuotientModule {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) [IsNoetherianRing (primitiveQuotientAlgebra e)ᵐᵒᵖ] (i : S.PrimitiveQuotientLabel D) :
              Module k ↑((S.primitiveQuotientAlmostSplitSkeleton D).obj i)
              Instances For
                source
                theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveArrowDescentQuotientTower {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) [IsNoetherianRing (primitiveQuotientAlgebra e)ᵐᵒᵖ] (i : S.PrimitiveQuotientLabel D) :
                IsScalarTower k (primitiveQuotientAlgebra e)ᵐᵒᵖ ↑((S.primitiveQuotientAlmostSplitSkeleton D).obj i)
                source
                noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientRadicalAmbientLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) [IsNoetherianRing (primitiveQuotientAlgebra e)ᵐᵒᵖ] (x y : S.PrimitiveQuotientLabel D) :
                ↥((S.primitiveQuotientAlmostSplitSkeleton D).radicalHom x y) ≃ₗ[k] ↥(S.almostSplitSkeleton.radicalHom ↑x ↑y)

                Inflation identifies the quotient and ambient radical spaces between surviving indecomposables.

                Instances For
                  source
                  theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientRadicalSquare_map_mem {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) [IsNoetherianRing (primitiveQuotientAlgebra e)ᵐᵒᵖ] (x y : S.PrimitiveQuotientLabel D) (f : ↥((S.primitiveQuotientAlmostSplitSkeleton D).radicalHom x y)) (hf : f ∈ (S.primitiveQuotientAlmostSplitSkeleton D).radicalSquareInRadicalSubmodule x y) :
                  (S.primitiveQuotientRadicalAmbientLinearEquiv D x y) f ∈ S.almostSplitSkeleton.radicalSquareInRadicalSubmodule ↑x ↑y

                  Every quotient radical-square factorization remains an ambient radical-square factorization after inflation.

                  source
                  noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveIrreducibleHomDescentLinearMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) [IsNoetherianRing (primitiveQuotientAlgebra e)ᵐᵒᵖ] (x y : S.PrimitiveQuotientLabel D) :
                  (S.primitiveQuotientAlmostSplitSkeleton D).irreducibleHomSpace x y →ₗ[k] S.almostSplitSkeleton.irreducibleHomSpace ↑x ↑y

                  The quotient-to-ambient map on irreducible morphism spaces.

                  Instances For
                    source
                    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveIrreducibleHomDescentLinearMap_surjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) [IsNoetherianRing (primitiveQuotientAlgebra e)ᵐᵒᵖ] (x y : S.PrimitiveQuotientLabel D) :
                    Function.Surjective ⇑(S.primitiveIrreducibleHomDescentLinearMap D x y)

                    Every ambient irreducible class between surviving modules has a quotient irreducible-class lift.

                    source
                    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientIrreducibleArrowMultiplicity_le_primitiveQuotient {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) [IsNoetherianRing (primitiveQuotientAlgebra e)ᵐᵒᵖ] (x y : S.PrimitiveQuotientLabel D) :
                    S.ambientIrreducibleArrowMultiplicity D x y ≤ S.primitiveQuotientIrreducibleArrowMultiplicity D x y

                    The first assertion of the manuscript's descent lemma: a_(A/AeA)(X,Y) ≥ a_A(X,Y) for surviving indecomposables.

                    source
                    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientIrreducibleArrowMultiplicity_eq_ambient_add_gain {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) [IsNoetherianRing (primitiveQuotientAlgebra e)ᵐᵒᵖ] (x y : S.PrimitiveQuotientLabel D) :
                    S.primitiveQuotientIrreducibleArrowMultiplicity D x y = S.ambientIrreducibleArrowMultiplicity D x y + S.primitiveArrowGain D x y

                    Pointwise, quotient arrow multiplicity is ambient multiplicity plus the defined arrow gain.

                    source
                    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.sum_primitiveQuotientIrreducibleArrowMultiplicity_eq_ambient_add_gain {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) [IsNoetherianRing (primitiveQuotientAlgebra e)ᵐᵒᵖ] :
                    ∑ x : S.PrimitiveQuotientLabel D, ∑ y : S.PrimitiveQuotientLabel D, S.primitiveQuotientIrreducibleArrowMultiplicity D x y = ∑ x : S.PrimitiveQuotientLabel D, ∑ y : S.PrimitiveQuotientLabel D, S.ambientIrreducibleArrowMultiplicity D x y + S.primitiveTotalArrowGain D

                    Summing the pointwise descent identity gives the manuscript's total internal-arrow relation a_B = a₀ + c.