Free mixed modules over a simple algebra #
Over a commutative algebra object of the ind-completion whose only ideals are the zero subobject and the whole algebra, the free modules on mixed sums of the unit and of an odd line are semisimple of finite length. Consequently subobjects, quotients and subquotients of objects whose free module is a mixed sum again have free modules that are mixed sums, and every epimorphism out of a free mixed module has a section.
The development runs in three steps.
- The regular module is simple. Submodules of the regular module
are exactly the ideals of the algebra: the intertwining law of a
module map
ginto the regular module says precisely that multiplication by the algebra against the image ofglands in that image, which isRS.isIdeal_mk_hom; simplicity of the algebra then leaves only the zero and the whole subobject, andRS.mono_iff_hom/RS.epi_iff_homcarry the conclusion back to the category of modules (RS.simple_regularMod). - The free module on the odd line is simple. Whiskering on the
right by the line is invertible up to the rotation
RS.OddLine.rotcoming from the square of the line, so a submodule of the free module on the line becomes, after twisting, a submodule of the regular module (RS.lineToRegular); whiskering by the line reflects both vanishing and invertibility, so simplicity transfers (RS.simple_freeMod_oddLine). The route taken is the direct one: no auto-equivalence of the category of modules is built, only the single twisting functor's action on objects and morphisms, and the coherence identityRS.rot_actsaying that the rotation intertwines an action with its double twist. - The free module on a mixed sum is a
RS.mixSumof copies of the regular module and of the free module on the line (RS.freeModMixIso), by peeling summands withRS.OddLine.mixSuccIsoandRS.OddLine.mixLineSuccIsoand carrying them across withRS.freeModBiprodIso.
The payoff combines these with the engine of
RS/Classical/Deligne/ModAbelian.lean: RS.exists_mixSum_iso_of_mono
and RS.exists_mixSum_iso_of_epi give
RS.exists_mix_of_mono_of_simple, RS.exists_mix_of_epi_of_simple
and RS.exists_mix_of_isSubquotient, since tensoring in Ind C is
exact and so the free-module functor preserves monomorphisms and
epimorphisms.
A last section splits epimorphisms. In any abelian category an
epimorphism out of a finite direct sum of simple objects has a
section (RS.exists_section_idxSum, from the binary step
RS.exists_section_biprod), so over a simple algebra every
epimorphism out of a free mixed module splits
(RS.exists_section_freeMod_mix), which supplies the section datum
of the local splitting statement without constructing it by hand.
Splitting epimorphisms out of a sum of simple objects #
The inductive step for splitting an epimorphism: an
epimorphism out of X ⊞ T with X simple splits as soon as every
epimorphism out of T splits. Either the second summand already
covers the target — the cokernel of its restriction vanishes — and
the section comes from the hypothesis on T; or the simple summand
maps isomorphically onto that cokernel, which exhibits the target as
the cokernel together with the image of the second summand, and the
two halves of the section are assembled by addition.
An epimorphism out of a finite direct sum of simple objects splits.
An epimorphism out of a sum of copies of two simple objects splits.
A module map is an isomorphism exactly when its underlying morphism is.
A submodule of the regular module is an ideal. The intertwining law of a module map into the regular module says exactly that multiplication by the algebra lands in the subobject.
The regular module over a simple algebra is simple: its submodules are exactly the ideals of the algebra.
Rotating by the odd line #
The rotation is compatible with whiskering on the left: a purely structural identity, once the square of the line is moved to a common position on both sides.
The rotation is compatible with whiskering on the left: a purely structural identity, once the square of the line is moved to a common position on both sides.
The rotation intertwines an action with its double twist by the line.
Whiskering by the line carries an intertwiner to an intertwiner for the twisted actions.
Whiskering by the line reflects isomorphisms.
The free module on the odd line #
A module twisted on the right by the odd line.
Equations
- RS.modLine 𝔹 L M = { X := CategoryTheory.MonoidalCategoryStruct.tensorObj M.X L.obj, mod := RS.tensorRightModObj 𝔹 M.X L.obj }
Instances For
A submodule of the free module on the line becomes a submodule of the regular module after twisting by the line: the twist of the free module on the line is the regular module, by the rotation.
Equations
Instances For
The twisted map vanishes exactly when the original does.
The free module on the odd line is nonzero as soon as the unit of the algebra is: the rotation identifies its double twist with the algebra.
The free module on the odd line over a simple algebra is simple. Twisting by the line carries its submodules to submodules of the regular module, and whiskering by the line reflects both vanishing and invertibility.
The free module on a mixed sum #
A module whose carrier vanishes vanishes.
The free module on a mixed sum is a mixed sum of copies of the regular module and of the free module on the odd line. The free-module functor carries the peeling isomorphisms of the mixed sum to biproduct decompositions of the module.
Equations
- One or more equations did not get rendered due to their size.
- RS.freeModMixIso 𝔹 L 0 0 = ⋯.iso ⋯
Instances For
Subquotients of a free mixed module #
The free-module functor preserves monomorphisms: tensoring in the ind-completion is exact.
The free-module functor preserves epimorphisms.
A subobject of an object with free mixed module has a free mixed module.
A quotient of an object with free mixed module has a free mixed module.
A subquotient of an object with free mixed module has a free mixed module.
Every epimorphism out of a free mixed module splits. Over a simple algebra a free mixed module is a finite direct sum of copies of two simple modules, and an epimorphism out of such a sum has a section.
A morphism whose source has a free mixed module has a module-level section as soon as its free module is an epimorphism. This is the section datum of the local splitting statement, supplied by semisimplicity rather than by hand.