Morphisms of Auslander–Bridger transposes

A commutative square between presenting arrows induces a map between their transposes in the opposite direction, by precomposing functional representatives. These maps preserve addition and reverse composition. Every map between modules lifts to a square between their projective presentations.

Different lifts of the same module map need not induce equal maps of transposes. Their difference factors through Hom_A(P₁, A), where P₁ is the source of the first presenting arrow. The same factorization holds for a lift of a module map factoring through a projective. For finitely generated projective P₁, its dual is finitely generated projective over Aᵐᵒᵖ; thus these factorizations are the lift independence and the vanishing on projective factorizations needed to define the transpose on stable morphisms.

Main results

• TauCeti.AuslanderReitenTranspose.map: the contravariant map induced by a presentation square.
• TauCeti.exists_lift_projective_presentation: a module map lifts to projective presentations.
• TauCeti.AuslanderReitenTranspose.exists_map_sub_eq_mk_comp: two lifts of the same module map differ through the dual of the first projective.
• TauCeti.AuslanderReitenTranspose.exists_map_eq_mk_comp_of_factor: a lift of a map factoring through a projective induces a map factoring through that dual.

References

• M. Auslander, M. Bridger, Stable module theory, Mem. Amer. Math. Soc. 94 (1969), Section 2.1.

def TauCeti.AuslanderReitenTranspose.map {A : Type u_1} [Ring A] {P₀ : Type u_2} {P₁ : Type u_3} {Q₀ : Type u_4} {Q₁ : Type u_5} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] [AddCommMonoid Q₀] [Module A Q₀] [AddCommMonoid Q₁] [Module A Q₁] {p : P₁ →ₗ[A] P₀} {q : Q₁ →ₗ[A] Q₀} (f₀ : P₀ →ₗ[A] Q₀) (f₁ : P₁ →ₗ[A] Q₁) (hf : f₀ ∘ₗ p = q ∘ₗ f₁) : AuslanderReitenTranspose q →ₗ[Aᵐᵒᵖ] AuslanderReitenTranspose p

A commutative square from p to q induces an opposite-linear map from Tr q to Tr p. On functional representatives it is precomposition with the map between the sources.

Equations

• TauCeti.AuslanderReitenTranspose.map f₀ f₁ hf = TauCeti.AuslanderReitenTranspose.lift q (TauCeti.AuslanderReitenTranspose.mk p ∘ₗ LinearMap.lcomp Aᵐᵒᵖ A f₁) ⋯

@[simp]

theorem TauCeti.AuslanderReitenTranspose.map_mk {A : Type u_1} [Ring A] {P₀ : Type u_2} {P₁ : Type u_3} {Q₀ : Type u_4} {Q₁ : Type u_5} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] [AddCommMonoid Q₀] [Module A Q₀] [AddCommMonoid Q₁] [Module A Q₁] {p : P₁ →ₗ[A] P₀} {q : Q₁ →ₗ[A] Q₀} (f₀ : P₀ →ₗ[A] Q₀) (f₁ : P₁ →ₗ[A] Q₁) (hf : f₀ ∘ₗ p = q ∘ₗ f₁) (φ : Module.Dual A Q₁) : (map f₀ f₁ hf) ((mk q) φ) = (mk p) (φ ∘ₗ f₁)

The transpose map on functional representatives.

@[simp]

theorem TauCeti.AuslanderReitenTranspose.map_comp_mk {A : Type u_1} [Ring A] {P₀ : Type u_2} {P₁ : Type u_3} {Q₀ : Type u_4} {Q₁ : Type u_5} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] [AddCommMonoid Q₀] [Module A Q₀] [AddCommMonoid Q₁] [Module A Q₁] {p : P₁ →ₗ[A] P₀} {q : Q₁ →ₗ[A] Q₀} (f₀ : P₀ →ₗ[A] Q₀) (f₁ : P₁ →ₗ[A] Q₁) (hf : f₀ ∘ₗ p = q ∘ₗ f₁) : map f₀ f₁ hf ∘ₗ mk q = mk p ∘ₗ LinearMap.lcomp Aᵐᵒᵖ A f₁

Precomposition followed by the quotient map is the transpose map followed by representatives.

@[simp]

theorem TauCeti.AuslanderReitenTranspose.map_id {A : Type u_1} [Ring A] {P₀ : Type u_2} {P₁ : Type u_3} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] {p : P₁ →ₗ[A] P₀} : map LinearMap.id LinearMap.id ⋯ = LinearMap.id

The identity square induces the identity on the transpose.

@[simp]

theorem TauCeti.AuslanderReitenTranspose.map_zero {A : Type u_1} [Ring A] {P₀ : Type u_2} {P₁ : Type u_3} {Q₀ : Type u_4} {Q₁ : Type u_5} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] [AddCommMonoid Q₀] [Module A Q₀] [AddCommMonoid Q₁] [Module A Q₁] {p : P₁ →ₗ[A] P₀} {q : Q₁ →ₗ[A] Q₀} (f₀ : P₀ →ₗ[A] Q₀) (hf : f₀ ∘ₗ p = q ∘ₗ 0) : map f₀ 0 hf = 0

A square whose map between the sources vanishes induces zero on transposes.

@[simp]

theorem TauCeti.AuslanderReitenTranspose.map_add {A : Type u_1} [Ring A] {P₀ : Type u_2} {P₁ : Type u_3} {Q₀ : Type u_4} {Q₁ : Type u_5} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] [AddCommMonoid Q₀] [Module A Q₀] [AddCommMonoid Q₁] [Module A Q₁] {p : P₁ →ₗ[A] P₀} {q : Q₁ →ₗ[A] Q₀} (f₀ g₀ : P₀ →ₗ[A] Q₀) (f₁ g₁ : P₁ →ₗ[A] Q₁) (hf : f₀ ∘ₗ p = q ∘ₗ f₁) (hg : g₀ ∘ₗ p = q ∘ₗ g₁) : map (f₀ + g₀) (f₁ + g₁) ⋯ = map f₀ f₁ hf + map g₀ g₁ hg

Transposition is additive on commutative squares.

@[simp]

theorem TauCeti.AuslanderReitenTranspose.map_comp_map {A : Type u_1} [Ring A] {P₀ : Type u_2} {P₁ : Type u_3} {Q₀ : Type u_4} {Q₁ : Type u_5} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] [AddCommMonoid Q₀] [Module A Q₀] [AddCommMonoid Q₁] [Module A Q₁] {p : P₁ →ₗ[A] P₀} {q : Q₁ →ₗ[A] Q₀} {R₀ : Type u_6} {R₁ : Type u_7} [AddCommMonoid R₀] [Module A R₀] [AddCommMonoid R₁] [Module A R₁] {r : R₁ →ₗ[A] R₀} (f₀ : P₀ →ₗ[A] Q₀) (f₁ : P₁ →ₗ[A] Q₁) (hf : f₀ ∘ₗ p = q ∘ₗ f₁) (g₀ : Q₀ →ₗ[A] R₀) (g₁ : Q₁ →ₗ[A] R₁) (hg : g₀ ∘ₗ q = r ∘ₗ g₁) : map f₀ f₁ hf ∘ₗ map g₀ g₁ hg = map (g₀ ∘ₗ f₀) (g₁ ∘ₗ f₁) ⋯

Transposition reverses composition of commutative squares.

theorem TauCeti.AuslanderReitenTranspose.exists_map_sub_eq_mk_comp {A : Type u_1} [Ring A] {P₀ : Type u_2} {P₁ : Type u_3} {Q₀ : Type u_4} {Q₁ : Type u_5} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] [AddCommGroup Q₀] [Module A Q₀] [AddCommGroup Q₁] [Module A Q₁] {p : P₁ →ₗ[A] P₀} {q : Q₁ →ₗ[A] Q₀} {N : Type u_6} [AddCommGroup N] [Module A N] {ρ : Q₀ →ₗ[A] N} [Module.Projective A P₀] (hq : Function.Exact ⇑q ⇑ρ) (f₀ g₀ : P₀ →ₗ[A] Q₀) (f₁ g₁ : P₁ →ₗ[A] Q₁) (hf : f₀ ∘ₗ p = q ∘ₗ f₁) (hg : g₀ ∘ₗ p = q ∘ₗ g₁) (hfg : ρ ∘ₗ f₀ = ρ ∘ₗ g₀) : ∃ (h : AuslanderReitenTranspose q →ₗ[Aᵐᵒᵖ] Module.Dual A P₁), map f₀ f₁ hf - map g₀ g₁ hg = mk p ∘ₗ h

Two presentation squares inducing the same map after augmentation have transpose maps whose difference factors through the dual of P₁, with the final factor the quotient map. When P₁ is finite projective, this is independence on stable morphisms.

theorem TauCeti.AuslanderReitenTranspose.exists_map_eq_mk_comp_of_factor {A : Type u_1} [Ring A] {P₀ : Type u_2} {P₁ : Type u_3} {Q₀ : Type u_4} {Q₁ : Type u_5} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] [AddCommGroup Q₀] [Module A Q₀] [AddCommGroup Q₁] [Module A Q₁] {p : P₁ →ₗ[A] P₀} {q : Q₁ →ₗ[A] Q₀} {N : Type u_6} [AddCommGroup N] [Module A N] {ρ : Q₀ →ₗ[A] N} [Module.Projective A P₀] {M : Type u_7} {C : Type u_8} [AddCommMonoid M] [Module A M] [AddCommMonoid C] [Module A C] [Module.Projective A C] {π : P₀ →ₗ[A] M} (hp : π ∘ₗ p = 0) (hq : Function.Exact ⇑q ⇑ρ) (hρ : Function.Surjective ⇑ρ) (i : M →ₗ[A] C) (j : C →ₗ[A] N) (f₀ : P₀ →ₗ[A] Q₀) (f₁ : P₁ →ₗ[A] Q₁) (hf : f₀ ∘ₗ p = q ∘ₗ f₁) (hfactor : ρ ∘ₗ f₀ = j ∘ₗ i ∘ₗ π) : ∃ (h : AuslanderReitenTranspose q →ₗ[Aᵐᵒᵖ] Module.Dual A P₁), map f₀ f₁ hf = mk p ∘ₗ h

If a module map factors through a projective, any lift to presentations induces a transpose map factoring through the dual of P₁. No minimality or finiteness is required.