Documentation

TauCeti.Algebra.Category.FGModuleCat.Cyclic

Cyclic modules and maps out of them #

Let A be a ring and let a : A. The cyclic right A-module A ⧸ aA is represented as the quotient of the regular module Aᵐᵒᵖ by the left ideal generated by op a, which is op (aA): right A-modules are left Aᵐᵒᵖ-modules.

A map of right A-modules out of A ⧸ aA is determined by the image m of the generator, which can be any element with m * a = 0, written op a • m = 0. When A is an algebra over a field k, evaluation at the generator is a k-linear equivalence; the k-vector space structure on morphisms is Mathlib's ModuleCat.linearOverField.

For the truncated polynomial algebra A = K[X]/(X ^ n) over a field K, with x the class of X and M_i = A ⧸ (x ^ i), the elements of M_j killed by x ^ i form a space of dimension min i j, so dim_K Hom(M_i, M_j) = min i j for j ≤ n.

Main definitions #

Main results #

source
@[reducible, inline]
noncomputable abbrev TauCeti.FGModuleCat.cyclicModule {A : Type u} [Ring A] (a : A) :
FGModuleCat Aᵐᵒᵖ

The cyclic right A-module A ⧸ aA, as a finitely generated Aᵐᵒᵖ-module: the quotient of the regular module Aᵐᵒᵖ by the left ideal generated by op a, which is op (aA).

Equations
Instances For

    Maps out of a cyclic module #

    source
    noncomputable def TauCeti.FGModuleCat.cyclicModuleLift {A : Type u} [Ring A] {M : Type u} [AddCommGroup M] [Module Aᵐᵒᵖ M] [Module.Finite Aᵐᵒᵖ M] (a : A) (m : M) (hm : MulOpposite.op a • m = 0) :
    cyclicModule a ⟶ ↧M

    The map of right A-modules A ⧸ aA ⟶ M sending the class of c to c • m, for an element m with op a • m = 0.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.FGModuleCat.cyclicModuleLift_mk {A : Type u} [Ring A] {M : Type u} [AddCommGroup M] [Module Aᵐᵒᵖ M] [Module.Finite Aᵐᵒᵖ M] (a : A) (m : M) (hm : MulOpposite.op a • m = 0) (c : Aᵐᵒᵖ) :
      (ModuleCat.Hom.hom (cyclicModuleLift a m hm).hom) (Submodule.Quotient.mk c) = c • m
      source
      theorem TauCeti.FGModuleCat.cyclicModule_hom_ext {A : Type u} [Ring A] {a : A} {N : FGModuleCat Aᵐᵒᵖ} {f g : cyclicModule a ⟶ N} (h : (ModuleCat.Hom.hom f.hom) (Submodule.Quotient.mk 1) = (ModuleCat.Hom.hom g.hom) (Submodule.Quotient.mk 1)) :
      f = g

      Two maps out of the cyclic module A ⧸ aA agree when they agree on the generator.

      source
      theorem TauCeti.FGModuleCat.cyclicModule_hom_ext_iff {A : Type u} [Ring A] {a : A} {N : FGModuleCat Aᵐᵒᵖ} {f g : cyclicModule a ⟶ N} :
      f = g ↔ (ModuleCat.Hom.hom f.hom) (Submodule.Quotient.mk 1) = (ModuleCat.Hom.hom g.hom) (Submodule.Quotient.mk 1)
      source
      theorem TauCeti.FGModuleCat.smul_cyclicModule_hom_mk_one_eq_zero {A : Type u} [Ring A] {a : A} {N : FGModuleCat Aᵐᵒᵖ} (f : cyclicModule a ⟶ N) :
      MulOpposite.op a • (ModuleCat.Hom.hom f.hom) (Submodule.Quotient.mk 1) = 0

      The image of the generator under a map out of A ⧸ aA is killed by op a.

      source
      noncomputable def TauCeti.FGModuleCat.cyclicModuleHomEquiv {A : Type u} [Ring A] {M : Type u} [AddCommGroup M] [Module Aᵐᵒᵖ M] [Module.Finite Aᵐᵒᵖ M] (k : Type w) [Field k] [Algebra k A] [Module k M] [IsScalarTower k Aᵐᵒᵖ M] (a : A) :
      (cyclicModule a ⟶ ↧M) ≃ₗ[k] ↥(DistribSMul.toLinearMap k M (MulOpposite.op a)).ker

      Maps out of a cyclic module. Evaluation at the generator is a k-linear equivalence between maps of right A-modules A ⧸ aA ⟶ M and elements of M killed by op a.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.FGModuleCat.cyclicModuleHomEquiv_apply_coe {A : Type u} [Ring A] {M : Type u} [AddCommGroup M] [Module Aᵐᵒᵖ M] [Module.Finite Aᵐᵒᵖ M] (k : Type w) [Field k] [Algebra k A] [Module k M] [IsScalarTower k Aᵐᵒᵖ M] (a : A) (f : cyclicModule a ⟶ ↧M) :
        ↑((cyclicModuleHomEquiv k a) f) = (ModuleCat.Hom.hom f.hom) (Submodule.Quotient.mk 1)
        source
        @[simp]
        theorem TauCeti.FGModuleCat.cyclicModuleHomEquiv_symm_apply {A : Type u} [Ring A] {M : Type u} [AddCommGroup M] [Module Aᵐᵒᵖ M] [Module.Finite Aᵐᵒᵖ M] (k : Type w) [Field k] [Algebra k A] [Module k M] [IsScalarTower k Aᵐᵒᵖ M] (a : A) (m : ↥(DistribSMul.toLinearMap k M (MulOpposite.op a)).ker) :
        (cyclicModuleHomEquiv k a).symm m = cyclicModuleLift a ↑m ⋯

        The truncated polynomial algebra K[X]/(X ^ n) #

        source
        theorem TauCeti.FGModuleCat.finrank_ker_smul_op_root_pow {K : Type u} [Field K] {n i j : ℕ} (hj : j ≤ n) :
        Module.finrank K ↥(DistribSMul.toLinearMap K ((AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ ⧸ Ideal.span {MulOpposite.op (AdjoinRoot.root (Polynomial.X ^ n) ^ j)}) (MulOpposite.op (AdjoinRoot.root (Polynomial.X ^ n) ^ i))).ker = min i j

        Over K[X]/(X ^ n), the elements of M_j killed by x ^ i form a space of dimension min i j: multiplication by x ^ i on M_j has cokernel M_(min i j).

        source
        theorem TauCeti.FGModuleCat.finrank_map_ker_smul_op_root_pow {K : Type u} [Field K] {n i j : ℕ} (hi : i ≤ n) (hj : j ≤ n) :
        Module.finrank K ↥(Submodule.map (↑K (Submodule.mkQ (Ideal.span {MulOpposite.op (AdjoinRoot.root (Polynomial.X ^ n) ^ j)}))) (DistribSMul.toLinearMap K (AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ (MulOpposite.op (AdjoinRoot.root (Polynomial.X ^ n) ^ i))).ker) = j - min j (n - i)

        Over K[X]/(X ^ n), with x the class of X and M_j = A ⧸ (x ^ j), the image in M_j of the annihilator x ^ (n - i) A of x ^ i has dimension j - min j (n - i), for i, j ≤ n.

        source
        theorem TauCeti.FGModuleCat.finrank_cyclicModule_hom_root_pow {K : Type u} [Field K] {n i j : ℕ} (hj : j ≤ n) :
        Module.finrank K (cyclicModule (AdjoinRoot.root (Polynomial.X ^ n) ^ i) ⟶ cyclicModule (AdjoinRoot.root (Polynomial.X ^ n) ^ j)) = min i j

        Morphisms between the cyclic modules of K[X]/(X ^ n). With x the class of X and M_i = A ⧸ (x ^ i), the space of maps M_i ⟶ M_j has dimension min i j for j ≤ n.