The radical of a preadditive category

The radical of a preadditive category is the categorical Jacobson radical: the morphism f : X ⟶ Y lies in TauCeti.jacobsonRadical X Y when 𝟙 X - f ≫ g is invertible for every g : Y ⟶ X. On a single object this is the usual characterization of the Jacobson radical of the ring CategoryTheory.End X, with which it is identified by TauCeti.jacobsonRadical_self_eq_jacobson, and the point of the definition is that the same formula makes sense between two different objects and produces a two-sided ideal of the category: a subgroup of each morphism group, absorbed by composition on either side.

Between objects with local endomorphism rings — the indecomposables of a Krull-Schmidt category — the radical is exactly the set of non-isomorphisms (TauCeti.mem_jacobsonRadical_iff_not_isIso). That is the description under which the radical is used: for indecomposable X and Y with X ≇ Y every morphism X ⟶ Y is radical (TauCeti.jacobsonRadical_eq_top), and inside X ⟶ X the radical is the set of non-units of the local ring End X (TauCeti.mem_jacobsonRadical_self_iff_not_isUnit). Only one of the two objects has to be indecomposable for the radical to be described by splitting: out of a local source it is the set of non-split monomorphisms (TauCeti.mem_jacobsonRadical_iff_not_isSplitMono) and into a local target the set of non-split epimorphisms (TauCeti.mem_jacobsonRadical_iff_not_isSplitEpi), so an irreducible morphism is in particular radical (TauCeti.IsIrreducibleMorphism.mem_jacobsonRadical).

The square of the radical, TauCeti.jacobsonRadicalSq X Y, is the subgroup generated by the composites X ⟶ Z ⟶ Y of two radical morphisms. It is again a two-sided ideal, contained in the radical. In a category with binary biproducts, between objects with local endomorphism rings, the morphisms lying in the radical but not in its square are exactly the irreducible ones (TauCeti.isIrreducibleMorphism_iff_mem_jacobsonRadical_and_notMem_jacobsonRadicalSq), which is the sense in which the quotient rad(X, Y) / rad²(X, Y) is the space of irreducible morphisms. An arrow of the Auslander-Reiten quiver is a basis vector of that quotient over the residue division rings End X / rad(End X) and End Y / rad(End Y), a bimodule structure that is not built here; this file supplies the two subgroups, their ideal properties and, over a linear category, their submodule views, and TauCeti.CategoryTheory.Preadditive.Radical.Quotient forms the underlying quotient on top of them.

The engine of the whole development is Jacobson's lemma in its categorical form (TauCeti.isIso_id_sub_comp_comm): for a : X ⟶ Y and b : Y ⟶ X, the endomorphism 𝟙 X - a ≫ b of X is invertible exactly when 𝟙 Y - b ≫ a is, by the same formula (𝟙 Y - b ≫ a)⁻¹ = 𝟙 Y + b ≫ (𝟙 X - a ≫ b)⁻¹ ≫ a that proves it for rings. It is what makes the definition of the radical left-right symmetric, and it is what makes the radical closed under addition, exactly as in the ring case.

Main definitions

• TauCeti.jacobsonRadical X Y: the radical rad(X, Y), an AddSubgroup (X ⟶ Y).
• TauCeti.jacobsonRadicalSq X Y: its square rad²(X, Y).
• TauCeti.jacobsonRadicalSubmodule k X Y and TauCeti.jacobsonRadicalSqSubmodule k X Y: the two of them over a k-linear category, as Submodule k (X ⟶ Y).
• TauCeti.jacobsonRadicalSubmoduleCongr: conjugation by a pair of isomorphisms of the source and the target, as a k-linear equivalence of radicals.

Main results

• TauCeti.isIso_id_sub_comp_comm: Jacobson's lemma for a preadditive category.
• TauCeti.mem_jacobsonRadical_iff_isIso_id_sub_comp_left: the radical is left-right symmetric, the defining condition TauCeti.mem_jacobsonRadical_iff_isIso_id_sub_comp_right being readable with the composite taken in either order.
• TauCeti.comp_mem_jacobsonRadical_left and TauCeti.comp_mem_jacobsonRadical_right: the radical is a two-sided ideal of the category.
• TauCeti.jacobsonRadical_self_eq_jacobson: on a single object the radical is the Jacobson radical of the endomorphism ring, Ring.jacobson (End X).
• TauCeti.mem_jacobsonRadical_iff_not_isIso: between objects with local endomorphism rings, the radical is the set of non-isomorphisms; TauCeti.jacobsonRadical_eq_top is the case of two non-isomorphic such objects, and TauCeti.mem_jacobsonRadical_self_iff_not_isUnit the case of one object, where it recovers the non-units of End X.
• TauCeti.mem_jacobsonRadical_iff_not_isSplitMono: out of an object with a local endomorphism ring the radical is the set of morphisms that are not split monomorphisms, with no hypothesis on the target, and dually TauCeti.mem_jacobsonRadical_iff_not_isSplitEpi into such an object.
• TauCeti.IsIrreducibleMorphism.mem_jacobsonRadical: an irreducible morphism out of an object with a local endomorphism ring is radical.
• TauCeti.jacobsonRadicalSq_le_iff: the universal property of the square of the radical, a subgroup contains it exactly when it contains every composite of two radical morphisms.
• TauCeti.jacobsonRadicalSq_le_jacobsonRadical, TauCeti.comp_mem_jacobsonRadicalSq_left and TauCeti.comp_mem_jacobsonRadicalSq_right: the square of the radical is a two-sided ideal contained in the radical.
• TauCeti.mem_jacobsonRadicalSq_iff_exists_comp: over a category with binary biproducts a member of the square is a single composite of two radical morphisms, not merely a sum of such.
• TauCeti.isIrreducibleMorphism_iff_mem_jacobsonRadical_and_notMem_jacobsonRadicalSq: between objects with local endomorphism rings, in a category with binary biproducts, a morphism is irreducible exactly when it lies in the radical but not in its square.
• TauCeti.smul_mem_jacobsonRadical and TauCeti.smul_mem_jacobsonRadicalSq: over a linear category both are stable under the scalar action, which is what the submodule views record.
• TauCeti.jacobsonRadicalSubmodule_map_homCongr and TauCeti.jacobsonRadicalSqSubmodule_map_homCongr: conjugation by isomorphisms of the source and the target carries the radical onto the radical and its square onto its square.

Implementation notes

The membership condition is stated with the categorical composition f ≫ g and the identity 𝟙 X, not through the ring CategoryTheory.End X, whose multiplication is composition in the opposite order. The two agree — f ≫ g is g * f in End X — but the ring spelling would make the left-right asymmetry of the definition into an artefact of a convention rather than a genuine symmetry to be proved. Where a proof does pass through the ring — to use the local-ring API of End X — it crosses between the two spellings by rewriting with CategoryTheory.End.one_def and CategoryTheory.End.mul_def rather than by definitional unfolding.

Jacobson's lemma is proved as a private one-directional helper carrying the explicit inverse and exposed as the equivalence isIso_id_sub_comp_comm; an instance form is impossible, since the two hypotheses IsIso (𝟙 X - a ≫ b) and IsIso (𝟙 Y - b ≫ a) each imply the other and would loop.

The identification of jacobsonRadical X X with Mathlib's Ring.jacobson (End X) goes through TauCeti.Ring.mem_jacobson_iff_isUnit_one_add_mul_left: Ring.jacobson is defined as the infimum of the maximal left ideals, and Mathlib's quasi-regularity characterization of it (Ideal.mem_jacobson_bot) is available only over a commutative ring, whereas End X is not commutative. The noncommutative characterization is the one Tau Ceti proves for the left-right symmetry of the radical, and it is exactly the defining condition used here.

The hypotheses [IsLocalRing (End X)] are the working form of "X is indecomposable": in a Krull-Schmidt category the two are equivalent, and IsLocalRing carries the Nontrivial hypothesis (𝟙 X ≠ 0) that rules out the zero object, on which every morphism is invertible and the radical would be everything.

References

• M. Auslander, I. Reiten, S. Smalø, Representation Theory of Artin Algebras, CUP (1995), V.7 ("the radical of a category").
• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, LMS Student Texts 65, CUP (2006), A.3 and IV.1.
• Quiver-representations roadmap, Layer 6, sublayer 6A: "the radical of the module category and irreducible morphisms. ... The radical of the module category (maps that are non-isomorphisms between indecomposables) and its square; the irreducible maps are rad / rad²."

Jacobson's lemma

theorem TauCeti.isIso_id_sub_comp_comm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (a : X ⟶ Y) (b : Y ⟶ X) : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.id X - CategoryTheory.CategoryStruct.comp a b) ↔ CategoryTheory.IsIso (CategoryTheory.CategoryStruct.id Y - CategoryTheory.CategoryStruct.comp b a)

Jacobson's lemma, as an equivalence: 𝟙 X - a ≫ b is invertible exactly when the composite taken in the other order gives an invertible 𝟙 Y - b ≫ a.

The radical

def TauCeti.jacobsonRadical {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X Y : C) : AddSubgroup (X ⟶ Y)

The radical of a preadditive category, rad(X, Y): the morphisms f : X ⟶ Y such that 𝟙 X - f ≫ g is invertible for every g : Y ⟶ X.

For X = Y this is the Jacobson radical of the ring CategoryTheory.End X, in its characterization by quasi-regularity; the definition here is the extension of that condition to a pair of objects, and it is a two-sided ideal of the category (TauCeti.comp_mem_jacobsonRadical_left, TauCeti.comp_mem_jacobsonRadical_right).

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.mem_jacobsonRadical_iff_isIso_id_sub_comp_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} : f ∈ jacobsonRadical X Y ↔ ∀ (g : Y ⟶ X), CategoryTheory.IsIso (CategoryTheory.CategoryStruct.id X - CategoryTheory.CategoryStruct.comp f g)

Membership in the radical, spelled out: the defining condition, with the arbitrary morphism g composed on the right of f. This is the interface of TauCeti.jacobsonRadical: it is deliberately not a simp lemma, since unfolding every radical membership into a quantified invertibility statement is not the normal form the consumers of the radical work in.

theorem TauCeti.mem_jacobsonRadical_iff_isIso_id_sub_comp_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} : f ∈ jacobsonRadical X Y ↔ ∀ (g : Y ⟶ X), CategoryTheory.IsIso (CategoryTheory.CategoryStruct.id Y - CategoryTheory.CategoryStruct.comp g f)

The radical is left-right symmetric: the defining condition may equally be read with the arbitrary morphism g composed on the left of f, on the identity of Y.

The radical is a two-sided ideal

theorem TauCeti.comp_mem_jacobsonRadical_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {W X Y : C} (h : W ⟶ X) {f : X ⟶ Y} (hf : f ∈ jacobsonRadical X Y) : CategoryTheory.CategoryStruct.comp h f ∈ jacobsonRadical W Y

Precomposing a radical morphism keeps it radical.

theorem TauCeti.comp_mem_jacobsonRadical_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y Z : C} {f : X ⟶ Y} (hf : f ∈ jacobsonRadical X Y) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f h ∈ jacobsonRadical X Z

Postcomposing a radical morphism keeps it radical.

On a single object: the Jacobson radical of the endomorphism ring

theorem TauCeti.mem_jacobsonRadical_self_iff_mem_jacobson {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X : C} {f : CategoryTheory.End X} : f ∈ jacobsonRadical X X ↔ f ∈ Ring.jacobson (CategoryTheory.End X)

On a single object the radical is the Jacobson radical of the endomorphism ring, in membership form: f : X ⟶ X is radical exactly when it lies in Ring.jacobson (End X).

The bridge is the elementwise description of the Jacobson radical of a possibly noncommutative ring, TauCeti.Ring.mem_jacobson_iff_isUnit_one_add_mul_left: the defining condition below is that description read through CategoryTheory.End.mul_def, the arbitrary g : X ⟶ X running over the negatives of the arbitrary ring element.

theorem TauCeti.jacobsonRadical_self_eq_jacobson {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : C) : jacobsonRadical X X = Submodule.toAddSubgroup (Ring.jacobson (CategoryTheory.End X))

On a single object the radical is the Jacobson radical of the endomorphism ring. This is TauCeti.mem_jacobsonRadical_self_iff_mem_jacobson as an equality of subgroups, the form in which rad(X, X) is handed to the ring theory of End X: the quotient by which Auslander-Reiten theory divides is End X ⧸ Ring.jacobson (End X), which is a division ring in the case that theory works in, that of an object with a local endomorphism ring, but not for an arbitrary object of an arbitrary preadditive category.

Radical morphisms are not invertible

theorem TauCeti.id_eq_zero_of_isIso_of_mem_jacobsonRadical {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} (hf : f ∈ jacobsonRadical X Y) [CategoryTheory.IsIso f] : CategoryTheory.CategoryStruct.id X = 0

An invertible radical morphism forces the identity of its source to vanish: the defining condition applied to the inverse says that 0 is invertible.

theorem TauCeti.not_isIso_of_mem_jacobsonRadical {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} (hX : CategoryTheory.CategoryStruct.id X ≠ 0) (hf : f ∈ jacobsonRadical X Y) : ¬CategoryTheory.IsIso f

A radical morphism out of an object with a nonzero identity is not an isomorphism.

Objects with local endomorphism rings

theorem TauCeti.mem_jacobsonRadical_iff_not_isSplitMono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} [IsLocalRing (CategoryTheory.End X)] {f : X ⟶ Y} : f ∈ jacobsonRadical X Y ↔ ¬CategoryTheory.IsSplitMono f

Out of an object with a local endomorphism ring the radical is the set of morphisms that are not split monomorphisms. Only the source is constrained: were f ≫ g a unit of End X for some g : Y ⟶ X then g composed with its inverse would be a retraction of f, so for a non-split f every f ≫ g is a nonunit and 𝟙 X - f ≫ g is invertible by locality; conversely a retraction of a radical f exhibits 𝟙 X itself as radical, which forces 𝟙 X = 0.

theorem TauCeti.mem_jacobsonRadical_iff_not_isSplitEpi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} [IsLocalRing (CategoryTheory.End Y)] {f : X ⟶ Y} : f ∈ jacobsonRadical X Y ↔ ¬CategoryTheory.IsSplitEpi f

Into an object with a local endomorphism ring the radical is the set of morphisms that are not split epimorphisms, the dual of TauCeti.mem_jacobsonRadical_iff_not_isSplitMono: here only the target is constrained, and the defining condition is read in its left-hand form TauCeti.mem_jacobsonRadical_iff_isIso_id_sub_comp_left, with g ≫ f an endomorphism of Y.

@[simp]

theorem TauCeti.mem_jacobsonRadical_iff_not_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} [IsLocalRing (CategoryTheory.End X)] [IsLocalRing (CategoryTheory.End Y)] {f : X ⟶ Y} : f ∈ jacobsonRadical X Y ↔ ¬CategoryTheory.IsIso f

Between objects with local endomorphism rings the radical is the set of non-isomorphisms. This is the description of rad(X, Y) for indecomposable X and Y under which it is used in Auslander-Reiten theory. It is the simp normal form of radical membership in that setting, unlike the defining TauCeti.mem_jacobsonRadical_iff_isIso_id_sub_comp_right.

theorem TauCeti.jacobsonRadical_eq_top {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} [IsLocalRing (CategoryTheory.End X)] [IsLocalRing (CategoryTheory.End Y)] (h : IsEmpty (X ≅ Y)) : jacobsonRadical X Y = ⊤

All morphisms between non-isomorphic objects with local endomorphism rings are radical.

theorem TauCeti.IsIrreducibleMorphism.mem_jacobsonRadical {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} [IsLocalRing (CategoryTheory.End X)] {f : X ⟶ Y} (hf : IsIrreducibleMorphism f) : f ∈ jacobsonRadical X Y

An irreducible morphism out of an object with a local endomorphism ring is radical, an irreducible morphism never being a split monomorphism.

theorem TauCeti.mem_jacobsonRadical_self_iff_not_isUnit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X : C} [IsLocalRing (CategoryTheory.End X)] {f : CategoryTheory.End X} : f ∈ jacobsonRadical X X ↔ ¬IsUnit f

On a single object with a local endomorphism ring the radical is the set of non-units of that ring — the unique maximal ideal of End X, in the form available without commutativity.

The square of the radical

def TauCeti.jacobsonRadicalSq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X Y : C) : AddSubgroup (X ⟶ Y)

The square of the radical, rad²(X, Y): the subgroup of X ⟶ Y generated by the composites X ⟶ Z ⟶ Y of two radical morphisms, over all objects Z.

The generating set is not itself a subgroup — a sum of two composites need not factor through a single object without biproducts — so the closure is taken.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.comp_mem_jacobsonRadicalSq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Z Y : C} {a : X ⟶ Z} {b : Z ⟶ Y} (ha : a ∈ jacobsonRadical X Z) (hb : b ∈ jacobsonRadical Z Y) : CategoryTheory.CategoryStruct.comp a b ∈ jacobsonRadicalSq X Y

A composite of two radical morphisms lies in the square of the radical.

@[simp]

theorem TauCeti.jacobsonRadicalSq_le_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {K : AddSubgroup (X ⟶ Y)} : jacobsonRadicalSq X Y ≤ K ↔ ∀ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), a ∈ jacobsonRadical X Z → b ∈ jacobsonRadical Z Y → CategoryTheory.CategoryStruct.comp a b ∈ K

The universal property of the square of the radical: an additive subgroup contains rad²(X, Y) exactly when it contains every composite of two radical morphisms.

This is the elimination rule matching the introduction rule TauCeti.comp_mem_jacobsonRadicalSq; together they let containments of rad² be proved without unfolding the closure that defines it, and it is the simp normal form of such a containment.

theorem TauCeti.jacobsonRadicalSq_le_jacobsonRadical {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X Y : C) : jacobsonRadicalSq X Y ≤ jacobsonRadical X Y

The square of the radical is contained in the radical, the radical being closed under composition.

theorem TauCeti.comp_mem_jacobsonRadicalSq_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {W X Y : C} (h : W ⟶ X) {f : X ⟶ Y} (hf : f ∈ jacobsonRadicalSq X Y) : CategoryTheory.CategoryStruct.comp h f ∈ jacobsonRadicalSq W Y

Precomposition preserves the square of the radical.

theorem TauCeti.comp_mem_jacobsonRadicalSq_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y Z : C} {f : X ⟶ Y} (hf : f ∈ jacobsonRadicalSq X Y) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f h ∈ jacobsonRadicalSq X Z

Postcomposition preserves the square of the radical.

Irreducible morphisms and the square of the radical

theorem TauCeti.mem_jacobsonRadicalSq_iff_exists_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Y : C} {f : X ⟶ Y} : f ∈ jacobsonRadicalSq X Y ↔ ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), a ∈ jacobsonRadical X Z ∧ b ∈ jacobsonRadical Z Y ∧ f = CategoryTheory.CategoryStruct.comp a b

An element of the square of the radical is a single composite of two radical morphisms, as soon as the category has binary biproducts: a sum a₁ ≫ b₁ + a₂ ≫ b₂ of two such composites is the single composite of CategoryTheory.Limits.biprod.lift a₁ a₂ with CategoryTheory.Limits.biprod.desc b₁ b₂ through Z₁ ⊞ Z₂, and those two factors are radical because the radical is a two-sided ideal closed under addition.

Without biproducts only the introduction rule TauCeti.comp_mem_jacobsonRadicalSq is available, which is why TauCeti.jacobsonRadicalSq is defined as the subgroup generated by the composites.

theorem TauCeti.isIrreducibleMorphism_iff_mem_jacobsonRadical_and_notMem_jacobsonRadicalSq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Y : C} [IsLocalRing (CategoryTheory.End X)] [IsLocalRing (CategoryTheory.End Y)] {f : X ⟶ Y} : IsIrreducibleMorphism f ↔ f ∈ jacobsonRadical X Y ∧ f ∉ jacobsonRadicalSq X Y

In a category with binary biproducts, between objects with local endomorphism rings the irreducible morphisms are exactly the morphisms in the radical but not in its square — the statement that the space of irreducible morphisms X ⟶ Y is rad(X, Y) / rad²(X, Y), which is what an arrow of the Auslander-Reiten quiver records.

Both directions run through the description of the radical by splitting (TauCeti.mem_jacobsonRadical_iff_not_isSplitMono and TauCeti.mem_jacobsonRadical_iff_not_isSplitEpi), each of which constrains only one of the two objects: in a factorization f = g ≫ h, the first factor fails to be a split mono exactly when it is radical, and the second fails to be a split epi exactly when it is radical. So the factorization clause of irreducibility says precisely that f is not a composite of two radical morphisms, which by TauCeti.mem_jacobsonRadicalSq_iff_exists_comp is membership in rad².

The radical of a linear category

theorem TauCeti.smul_mem_jacobsonRadical {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {k : Type u_1} [Semiring k] [CategoryTheory.Linear k C] {X Y : C} (c : k) {f : X ⟶ Y} (hf : f ∈ jacobsonRadical X Y) : c • f ∈ jacobsonRadical X Y

Scaling a radical morphism keeps it radical: in a linear category a scalar moves across a composite, so scaling f has the same effect on the defining condition as scaling the arbitrary morphism it is tested against.

theorem TauCeti.smul_mem_jacobsonRadicalSq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {k : Type u_1} [Semiring k] [CategoryTheory.Linear k C] {X Y : C} (c : k) {f : X ⟶ Y} (hf : f ∈ jacobsonRadicalSq X Y) : c • f ∈ jacobsonRadicalSq X Y

Scaling preserves the square of the radical, the generating composites being scaled in their first factor.

def TauCeti.jacobsonRadicalSubmodule {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type u_1) [Semiring k] [CategoryTheory.Linear k C] (X Y : C) : Submodule k (X ⟶ Y)

The radical of a k-linear category as a submodule, the same subgroup as TauCeti.jacobsonRadical with its scalar action recorded. It is this view, and that of the square below, that the quotient rad(X, Y) / rad²(X, Y) behind an arrow of the Auslander-Reiten quiver is formed in.

Equations

• TauCeti.jacobsonRadicalSubmodule k X Y = { carrier := ↑(TauCeti.jacobsonRadical X Y), add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

def TauCeti.jacobsonRadicalSqSubmodule {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type u_1) [Semiring k] [CategoryTheory.Linear k C] (X Y : C) : Submodule k (X ⟶ Y)

The square of the radical of a k-linear category as a submodule, the same subgroup as TauCeti.jacobsonRadicalSq.

Equations

• TauCeti.jacobsonRadicalSqSubmodule k X Y = { carrier := ↑(TauCeti.jacobsonRadicalSq X Y), add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem TauCeti.mem_jacobsonRadicalSubmodule {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {k : Type u_1} [Semiring k] [CategoryTheory.Linear k C] {X Y : C} {f : X ⟶ Y} : f ∈ jacobsonRadicalSubmodule k X Y ↔ f ∈ jacobsonRadical X Y

The submodule view of the radical has the same members as the subgroup.

@[simp]

theorem TauCeti.mem_jacobsonRadicalSqSubmodule {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {k : Type u_1} [Semiring k] [CategoryTheory.Linear k C] {X Y : C} {f : X ⟶ Y} : f ∈ jacobsonRadicalSqSubmodule k X Y ↔ f ∈ jacobsonRadicalSq X Y

The submodule view of the square of the radical has the same members as the subgroup.

theorem TauCeti.jacobsonRadicalSqSubmodule_le_jacobsonRadicalSubmodule {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {k : Type u_1} [Semiring k] [CategoryTheory.Linear k C] (X Y : C) : jacobsonRadicalSqSubmodule k X Y ≤ jacobsonRadicalSubmodule k X Y

The square of the radical is contained in the radical, as submodules of a linear category.

Conjugation of the radical by a pair of isomorphisms

@[simp]

theorem TauCeti.jacobsonRadicalSubmodule_map_homCongr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type u_1) [Semiring k] [CategoryTheory.Linear k C] {X X' Y Y' : C} (e : X ≅ X') (e' : Y ≅ Y') : Submodule.map (↑(CategoryTheory.Linear.homCongr k e e')) (jacobsonRadicalSubmodule k X Y) = jacobsonRadicalSubmodule k X' Y'

Conjugation by isomorphisms carries the radical onto the radical. Both containments are the radical being a two-sided ideal of the category: e.inv ≫ f ≫ e'.hom is radical whenever f is, and the reverse containment is the same statement for the inverse conjugation e.hom ≫ g ≫ e'.inv.

@[simp]

theorem TauCeti.jacobsonRadicalSqSubmodule_map_homCongr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type u_1) [Semiring k] [CategoryTheory.Linear k C] {X X' Y Y' : C} (e : X ≅ X') (e' : Y ≅ Y') : Submodule.map (↑(CategoryTheory.Linear.homCongr k e e')) (jacobsonRadicalSqSubmodule k X Y) = jacobsonRadicalSqSubmodule k X' Y'

Conjugation by isomorphisms carries the square of the radical onto the square of the radical, the square being a two-sided ideal of the category just as the radical is.

noncomputable def TauCeti.jacobsonRadicalSubmoduleCongr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type u_1) [Semiring k] [CategoryTheory.Linear k C] {X X' Y Y' : C} (e : X ≅ X') (e' : Y ≅ Y') : ↥(jacobsonRadicalSubmodule k X Y) ≃ₗ[k] ↥(jacobsonRadicalSubmodule k X' Y')

Conjugation by isomorphisms, as an equivalence of radicals.

Equations

• TauCeti.jacobsonRadicalSubmoduleCongr k e e' = (CategoryTheory.Linear.homCongr k e e').ofSubmodules (TauCeti.jacobsonRadicalSubmodule k X Y) (TauCeti.jacobsonRadicalSubmodule k X' Y') ⋯

@[simp]

theorem TauCeti.coe_jacobsonRadicalSubmoduleCongr_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type u_1) [Semiring k] [CategoryTheory.Linear k C] {X X' Y Y' : C} (e : X ≅ X') (e' : Y ≅ Y') (f : ↥(jacobsonRadicalSubmodule k X Y)) : ↑((jacobsonRadicalSubmoduleCongr k e e') f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp e.inv ↑f) e'.hom

Conjugation acts on radical morphisms by conjugation: the morphism underlying the image of f is e.inv ≫ f ≫ e'.hom.

@[simp]

theorem TauCeti.coe_jacobsonRadicalSubmoduleCongr_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type u_1) [Semiring k] [CategoryTheory.Linear k C] {X X' Y Y' : C} (e : X ≅ X') (e' : Y ≅ Y') (g : ↥(jacobsonRadicalSubmodule k X' Y')) : ↑((jacobsonRadicalSubmoduleCongr k e e').symm g) = CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.CategoryStruct.comp (↑g) e'.inv)

The inverse conjugation acts by the inverse conjugation: the morphism underlying the preimage of g is e.hom ≫ g ≫ e'.inv.