Documentation

TauCeti.Algebra.Module.Projective.LinearMap

Hom spaces out of a projective module #

Let k be a field and A a k-algebra. For a projective A-module P the functor Hom_A(P, -) is exact, so when P and the targets are finite-dimensional over k the dimension dim_k Hom_A(P, -) is additive across a submodule and its quotient.

Exactness of Hom_A(P, -) also computes the maps from P into a reduction V ⧸ x • V, for A an algebra over a commutative ring R and x : R a non-zero-divisor on V: they are the reductions modulo x of the maps P → V. Over R = ℤ_p and x = p, this makes the number of maps from a projective ℤ_p[G]-lattice into the reduction of another lattice a function of the ℤ_p-module of maps between the lattices.

Main results #

source
theorem TauCeti.finrank_linearMap_quotient_add_finrank_linearMap (k : Type u_1) {A : Type u_2} (P : Type u_3) {M : Type u_4} [Field k] [Ring A] [Algebra k A] [AddCommGroup P] [Module k P] [Module A P] [IsScalarTower k A P] [FiniteDimensional k P] [Module.Projective A P] [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [FiniteDimensional k M] (N : Submodule A M) :
Module.finrank k (P →ₗ[A] M ⧸ N) + Module.finrank k (P →ₗ[A] ↥N) = Module.finrank k (P →ₗ[A] M)

dim_k Hom_A(P, -) is additive, for P projective and finite-dimensional over k: the functor Hom_A(P, -) is exact, so a submodule and its quotient split the dimension of the hom space out of P.

source
theorem TauCeti.ker_compRight_mkQ_eq_smul_top {R : Type u_5} {A : Type u_6} (P : Type u_7) {V : Type u_8} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup P] [Module A P] [AddCommGroup V] [Module R V] [Module A V] [IsScalarTower R A V] {x : R} (hx : IsSMulRegular V x) :
(LinearMap.compRight R (Ideal.span {(algebraMap R A) x} • ⊤).mkQ).ker = x • ⊤

Maps into x • V are multiples of x. For x : R a non-zero-divisor on the A-module V, a map P → V reduces to zero in V ⧸ x • V exactly when it is x times a map P → V.

source
theorem TauCeti.compRight_mkQ_surjective (R : Type u_5) {A : Type u_6} (P : Type u_7) {V : Type u_8} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup P] [Module A P] [AddCommGroup V] [Module R V] [Module A V] [IsScalarTower R A V] [Module.Projective A P] (N : Submodule A V) :
Function.Surjective ⇑(LinearMap.compRight R N.mkQ)

Maps from a projective module into a quotient lift. For P projective, every map P → V ⧸ N is the reduction of a map P → V.

source
noncomputable def TauCeti.quotientSMulTopLinearMapEquiv {R : Type u_5} {A : Type u_6} (P : Type u_7) {V : Type u_8} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup P] [Module A P] [AddCommGroup V] [Module R V] [Module A V] [IsScalarTower R A V] {x : R} [Module.Projective A P] (hx : IsSMulRegular V x) :
((P →ₗ[A] V) ⧸ x • ⊤) ≃ₗ[R] P →ₗ[A] V ⧸ Ideal.span {(algebraMap R A) x} • ⊤

Maps from a projective module into a reduction. Let A be an algebra over a commutative ring R, let P be a projective A-module, and let x : R be a non-zero-divisor on the A-module V. Composition with V → V ⧸ x • V identifies the maps P → V ⧸ x • V with the reductions modulo x of the maps P → V: every map lifts because P is projective, and a map with values in x • V is x times a map.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.quotientSMulTopLinearMapEquiv_mk {R : Type u_5} {A : Type u_6} {P : Type u_7} {V : Type u_8} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup P] [Module A P] [AddCommGroup V] [Module R V] [Module A V] [IsScalarTower R A V] {x : R} [Module.Projective A P] (hx : IsSMulRegular V x) (f : P →ₗ[A] V) :
    (quotientSMulTopLinearMapEquiv P hx) (Submodule.Quotient.mk f) = (Ideal.span {(algebraMap R A) x} • ⊤).mkQ ∘ₗ f