The Auslander--Reiten transpose

Given a projective presentation P₁ → P₀ → M, applying Hom_A(-, A) reverses the first map. The cokernel

Hom_A(P₁, A) / range(Hom_A(P₀, A) → Hom_A(P₁, A))

is the Auslander--Reiten transpose of the presentation. It is naturally a left module over the opposite ring Aᵐᵒᵖ: an element op a acts on a functional by multiplication by a on the right. Mathlib already supplies this opposite-ring module structure on Module.Dual A P and the precomposition map as p.lcomp Aᵐᵒᵖ A; this file forms its cokernel rather than rebuilding either.

The transpose is independent, up to linear equivalence, of the chosen minimal projective presentation. More precisely, an isomorphism of presentation diagrams induces an equivalence of the two cokernels (AuslanderReitenTranspose.linearEquiv), characterized on representatives, and the uniqueness theorem for minimal presentations then gives IsMinimalProjectivePresentation.nonempty_linearEquiv_auslanderReitenTranspose.

The construction is additive in the presenting arrow: AuslanderReitenTranspose.prodMapEquiv identifies the transpose of a direct sum with the product of the two transposes, while AuslanderReitenTranspose.compFstEquiv identifies the transpose of an arrow enlarged by a zero source summand with the product of its transpose and the dual of that summand.

The transpose is a construction on the non-projective modules: for a minimal projective presentation P₁ → P₀ → M whose left-hand source P₁ is finitely generated, it vanishes on a projective M and on no other, which is IsMinimalProjectivePresentation.subsingleton_auslanderReitenTranspose_iff_projective.

This supplies the transpose construction in sublayer 6C of the quiver-representations roadmap. The remaining part of 6C develops its stable equivalence; sublayer 6D applies the duality D = Hom_k(-, k) to construct the Auslander--Reiten translate τ = D Tr, in TauCeti/Algebra/Module/AuslanderReiten/Translate.lean. The scalar structure that duality dualizes over — a base ring k of A acting on the transpose through Aᵐᵒᵖ — is supplied here, next to the other module structures on the transpose.

Main definitions

• AuslanderReitenTranspose: the cokernel of the dual of the first map in a projective presentation.
• AuslanderReitenTranspose.lift: the universal property of that cokernel, descending an opposite-linear map that kills the functionals factoring through p₁.
• AuslanderReitenTranspose.linearEquiv: the equivalence induced by an isomorphism of presentation diagrams.
• AuslanderReitenTranspose.prodMapEquiv: the transpose of a direct sum of arrows is the direct sum of their transposes.
• AuslanderReitenTranspose.compFstEquiv: a zero source summand contributes its dual to the transpose.

Main results

• AuslanderReitenTranspose.subsingleton_iff_exists_comp_eq_id: for a finitely generated projective P₁, the transpose of p₁ vanishes exactly when p₁ is a split monomorphism.
• IsMinimalProjectivePresentation.subsingleton_auslanderReitenTranspose_iff_projective: for a minimal projective presentation with finitely generated left-hand source, the transpose vanishes exactly on the projective modules. The forward direction is IsMinimalProjectivePresentation.subsingleton_auslanderReitenTranspose_of_projective and needs no finiteness; the converse is IsMinimalProjectivePresentation.projective_of_subsingleton_auslanderReitenTranspose, and asks the left-hand source of the presentation to be finitely generated, which it is over an Artin algebra once the presented module is.
• IsMinimalProjectivePresentation.nonempty_linearEquiv_auslanderReitenTranspose: the transpose does not depend on the chosen minimal presentation.

References

• M. Auslander, I. Reiten, S. O. Smalø, Representation Theory of Artin Algebras, Cambridge University Press (1995), Section IV.1.
• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Cambridge University Press (2006), Section IV.2.

def TauCeti.AuslanderReitenTranspose {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) : Type (max (max u w) w u)

The Auslander--Reiten transpose attached to a projective presentation whose first map is p₁ : P₁ → P₀. It is the cokernel of the opposite-linear precomposition map Hom_A(P₀, A) → Hom_A(P₁, A).

Minimality is not needed to form the cokernel. It is used by IsMinimalProjectivePresentation.nonempty_linearEquiv_auslanderReitenTranspose to show that the result is independent, up to equivalence, of the chosen presentation of a module.

Equations

• TauCeti.AuslanderReitenTranspose p₁ = (Module.Dual A P₁ ⧸ (LinearMap.lcomp Aᵐᵒᵖ A p₁).range)

@[instance_reducible]

instance TauCeti.AuslanderReitenTranspose.instAddCommGroup {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) : AddCommGroup (AuslanderReitenTranspose p₁)

Equations

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

@[instance_reducible]

instance TauCeti.AuslanderReitenTranspose.instModuleMulOpposite {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) : Module Aᵐᵒᵖ (AuslanderReitenTranspose p₁)

Equations

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

@[instance_reducible]

instance TauCeti.AuslanderReitenTranspose.instModule {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) (k : Type u_1) [CommSemiring k] [Algebra k A] : Module k (AuslanderReitenTranspose p₁)

A base ring k of A acts on the transpose, through the algebra map into Aᵐᵒᵖ. This is the scalar structure the Auslander--Reiten translate dualizes over.

Equations

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

instance TauCeti.AuslanderReitenTranspose.instIsScalarTowerMulOpposite {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) (k : Type u_1) [CommSemiring k] [Algebra k A] : IsScalarTower k Aᵐᵒᵖ (AuslanderReitenTranspose p₁)

instance TauCeti.AuslanderReitenTranspose.instSMulCommClassMulOpposite {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) (k : Type u_1) [CommSemiring k] [Algebra k A] : SMulCommClass Aᵐᵒᵖ k (AuslanderReitenTranspose p₁)

@[simp]

theorem TauCeti.AuslanderReitenTranspose.op_algebraMap_smul {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) (k : Type u_1) [CommSemiring k] [Algebra k A] (c : k) (x : AuslanderReitenTranspose p₁) : MulOpposite.op ((algebraMap k A) c) • x = c • x

A scalar of k, viewed in Aᵐᵒᵖ through the algebra map, acts on the transpose as it does through the k-action itself.

def TauCeti.AuslanderReitenTranspose.mk {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) : Module.Dual A P₁ →ₗ[Aᵐᵒᵖ] AuslanderReitenTranspose p₁

The quotient map from the dual of the first projective onto its Auslander--Reiten transpose.

Equations

• TauCeti.AuslanderReitenTranspose.mk p₁ = (LinearMap.lcomp Aᵐᵒᵖ A p₁).range.mkQ

@[simp]

theorem TauCeti.AuslanderReitenTranspose.mk_eq_zero_iff {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) (φ : Module.Dual A P₁) : (mk p₁) φ = 0 ↔ φ ∈ (LinearMap.lcomp Aᵐᵒᵖ A p₁).range

A functional represents zero in the transpose exactly when it factors through the first map of the presentation.

@[simp]

theorem TauCeti.AuslanderReitenTranspose.ker_mk {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) : (mk p₁).ker = (LinearMap.lcomp Aᵐᵒᵖ A p₁).range

The quotient map onto the transpose kills exactly the functionals factoring through the first map of the presentation.

@[simp]

theorem TauCeti.AuslanderReitenTranspose.mk_lcomp {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) (φ : Module.Dual A P₀) : (mk p₁) ((LinearMap.lcomp Aᵐᵒᵖ A p₁) φ) = 0

A functional precomposed with the first map of the presentation vanishes in its cokernel.

theorem TauCeti.AuslanderReitenTranspose.mk_surjective {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) : Function.Surjective ⇑(mk p₁)

Every element of the transpose is represented by a functional on P₁.

@[simp]

theorem TauCeti.AuslanderReitenTranspose.mk_eq_mk_iff {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) (φ ψ : Module.Dual A P₁) : (mk p₁) φ = (mk p₁) ψ ↔ φ - ψ ∈ (LinearMap.lcomp Aᵐᵒᵖ A p₁).range

Two functionals represent the same element of the transpose exactly when their difference factors through the first map of the presentation.

theorem TauCeti.AuslanderReitenTranspose.induction_on {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) {motive : AuslanderReitenTranspose p₁ → Prop} (x : AuslanderReitenTranspose p₁) (h : ∀ (φ : Module.Dual A P₁), motive ((mk p₁) φ)) : motive x

To prove a property of every element of the transpose it suffices to prove it of the classes of functionals on P₁.

def TauCeti.AuslanderReitenTranspose.quotientEquiv {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) {S : Type u_1} {N : Type u_2} [Ring S] [AddCommGroup N] [Module S N] {σ : Aᵐᵒᵖ →+* S} {σ' : S →+* Aᵐᵒᵖ} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (Q : Submodule S N) (e : Module.Dual A P₁ ≃ₛₗ[σ] N) (he : Submodule.map (↑e) (LinearMap.lcomp Aᵐᵒᵖ A p₁).range = Q) : AuslanderReitenTranspose p₁ ≃ₛₗ[σ] N ⧸ Q

A semilinear equivalence carrying the range of precomposition onto Q identifies the transpose with the quotient by Q.

Equations

• TauCeti.AuslanderReitenTranspose.quotientEquiv p₁ Q e he = Submodule.Quotient.equiv (LinearMap.lcomp Aᵐᵒᵖ A p₁).range Q e he

@[simp]

theorem TauCeti.AuslanderReitenTranspose.quotientEquiv_mk {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) {S : Type u_1} {N : Type u_2} [Ring S] [AddCommGroup N] [Module S N] {σ : Aᵐᵒᵖ →+* S} {σ' : S →+* Aᵐᵒᵖ} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (Q : Submodule S N) (e : Module.Dual A P₁ ≃ₛₗ[σ] N) (he : Submodule.map (↑e) (LinearMap.lcomp Aᵐᵒᵖ A p₁).range = Q) (φ : Module.Dual A P₁) : (quotientEquiv p₁ Q e he) ((mk p₁) φ) = Submodule.Quotient.mk (e φ)

Quotient transport applies the semilinear equivalence to a functional representative.

@[simp]

theorem TauCeti.AuslanderReitenTranspose.quotientEquiv_symm_mk {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) {S : Type u_1} {N : Type u_2} [Ring S] [AddCommGroup N] [Module S N] {σ : Aᵐᵒᵖ →+* S} {σ' : S →+* Aᵐᵒᵖ} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (Q : Submodule S N) (e : Module.Dual A P₁ ≃ₛₗ[σ] N) (he : Submodule.map (↑e) (LinearMap.lcomp Aᵐᵒᵖ A p₁).range = Q) (n : N) : (quotientEquiv p₁ Q e he).symm (Submodule.Quotient.mk n) = (mk p₁) (e.symm n)

Inverse quotient transport applies the inverse equivalence to a quotient representative.

def TauCeti.AuslanderReitenTranspose.lift {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) {N : Type u_1} [AddCommGroup N] [Module Aᵐᵒᵖ N] (f : Module.Dual A P₁ →ₗ[Aᵐᵒᵖ] N) (hf : ∀ (φ : Module.Dual A P₀), f ((LinearMap.lcomp Aᵐᵒᵖ A p₁) φ) = 0) : AuslanderReitenTranspose p₁ →ₗ[Aᵐᵒᵖ] N

The universal property of the transpose: an opposite-linear map out of Hom_A(P₁, A) that kills every functional factoring through p₁ descends to the cokernel.

Equations

• TauCeti.AuslanderReitenTranspose.lift p₁ f hf = (LinearMap.lcomp Aᵐᵒᵖ A p₁).range.liftQ f ⋯

@[simp]

theorem TauCeti.AuslanderReitenTranspose.lift_mk {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) {N : Type u_1} [AddCommGroup N] [Module Aᵐᵒᵖ N] (f : Module.Dual A P₁ →ₗ[Aᵐᵒᵖ] N) (hf : ∀ (φ : Module.Dual A P₀), f ((LinearMap.lcomp Aᵐᵒᵖ A p₁) φ) = 0) (φ : Module.Dual A P₁) : (lift p₁ f hf) ((mk p₁) φ) = f φ

@[simp]

theorem TauCeti.AuslanderReitenTranspose.lift_comp_mk {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) {N : Type u_1} [AddCommGroup N] [Module Aᵐᵒᵖ N] (f : Module.Dual A P₁ →ₗ[Aᵐᵒᵖ] N) (hf : ∀ (φ : Module.Dual A P₀), f ((LinearMap.lcomp Aᵐᵒᵖ A p₁) φ) = 0) : lift p₁ f hf ∘ₗ mk p₁ = f

AuslanderReitenTranspose.lift factors the given map through the quotient map.

theorem TauCeti.AuslanderReitenTranspose.hom_ext {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) {N : Type u_1} [AddCommGroup N] [Module Aᵐᵒᵖ N] {f g : AuslanderReitenTranspose p₁ →ₗ[Aᵐᵒᵖ] N} (h : ∀ (φ : Module.Dual A P₁), f ((mk p₁) φ) = g ((mk p₁) φ)) : f = g

Opposite-linear maps out of the transpose are determined by their values on representatives.

theorem TauCeti.AuslanderReitenTranspose.hom_ext_iff {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] {p₁ : P₁ →ₗ[A] P₀} {N : Type u_1} [AddCommGroup N] [Module Aᵐᵒᵖ N] {f g : AuslanderReitenTranspose p₁ →ₗ[Aᵐᵒᵖ] N} : f = g ↔ ∀ (φ : Module.Dual A P₁), f ((mk p₁) φ) = g ((mk p₁) φ)

theorem TauCeti.AuslanderReitenTranspose.eq_lift {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) {N : Type u_1} [AddCommGroup N] [Module Aᵐᵒᵖ N] (f : Module.Dual A P₁ →ₗ[Aᵐᵒᵖ] N) (hf : ∀ (φ : Module.Dual A P₀), f ((LinearMap.lcomp Aᵐᵒᵖ A p₁) φ) = 0) (g : AuslanderReitenTranspose p₁ →ₗ[Aᵐᵒᵖ] N) (hg : ∀ (φ : Module.Dual A P₁), g ((mk p₁) φ) = f φ) : g = lift p₁ f hf

AuslanderReitenTranspose.lift is the unique descent of f to the transpose.

def TauCeti.AuslanderReitenTranspose.prodMapEquiv {A : Type u} [Ring A] {A₁ : Type u_1} {A₂ : Type u_2} {E₁ : Type u_3} {E₂ : Type u_4} [AddCommMonoid A₁] [Module A A₁] [AddCommMonoid A₂] [Module A A₂] [AddCommMonoid E₁] [Module A E₁] [AddCommMonoid E₂] [Module A E₂] (u : A₁ →ₗ[A] E₁) (w : A₂ →ₗ[A] E₂) : AuslanderReitenTranspose (u.prodMap w) ≃ₗ[Aᵐᵒᵖ] AuslanderReitenTranspose u × AuslanderReitenTranspose w

The transpose is additive. The transpose of the direct sum u ⊕ w of two arrows is the direct sum of their transposes. On representatives it restricts a functional on A₁ × A₂ to the two summands.

Equations

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

@[simp]

theorem TauCeti.AuslanderReitenTranspose.prodMapEquiv_mk {A : Type u} [Ring A] {A₁ : Type u_1} {A₂ : Type u_2} {E₁ : Type u_3} {E₂ : Type u_4} [AddCommMonoid A₁] [Module A A₁] [AddCommMonoid A₂] [Module A A₂] [AddCommMonoid E₁] [Module A E₁] [AddCommMonoid E₂] [Module A E₂] (u : A₁ →ₗ[A] E₁) (w : A₂ →ₗ[A] E₂) (φ : Module.Dual A (A₁ × A₂)) : (prodMapEquiv u w) ((mk (u.prodMap w)) φ) = ((mk u) (φ ∘ₗ LinearMap.inl A A₁ A₂), (mk w) (φ ∘ₗ LinearMap.inr A A₁ A₂))

The equivalence prodMapEquiv restricts a representative to the two summands.

@[simp]

theorem TauCeti.AuslanderReitenTranspose.prodMapEquiv_symm_mk {A : Type u} [Ring A] {A₁ : Type u_1} {A₂ : Type u_2} {E₁ : Type u_3} {E₂ : Type u_4} [AddCommMonoid A₁] [Module A A₁] [AddCommMonoid A₂] [Module A A₂] [AddCommMonoid E₁] [Module A E₁] [AddCommMonoid E₂] [Module A E₂] (u : A₁ →ₗ[A] E₁) (w : A₂ →ₗ[A] E₂) (φ : Module.Dual A A₁) (ψ : Module.Dual A A₂) : (prodMapEquiv u w).symm ((mk u) φ, (mk w) ψ) = (mk (u.prodMap w)) (LinearMap.coprod φ ψ)

The inverse of prodMapEquiv combines representatives using the canonical functional on the product.

def TauCeti.AuslanderReitenTranspose.compFstEquiv {A : Type u} [Ring A] {A₁ : Type u_1} {E₁ : Type u_3} [AddCommMonoid A₁] [Module A A₁] [AddCommMonoid E₁] [Module A E₁] (u : A₁ →ₗ[A] E₁) (C : Type u_5) [AddCommMonoid C] [Module A C] : AuslanderReitenTranspose (u ∘ₗ LinearMap.fst A A₁ C) ≃ₗ[Aᵐᵒᵖ] AuslanderReitenTranspose u × Module.Dual A C

A zero summand contributes its dual. Enlarging the source of u : A₁ → E₁ by a summand C on which the arrow vanishes adds Hom_A(C, A) to the transpose. On representatives it restricts a functional on A₁ × C to the two summands.

Equations

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

@[simp]

theorem TauCeti.AuslanderReitenTranspose.compFstEquiv_mk {A : Type u} [Ring A] {A₁ : Type u_1} {E₁ : Type u_3} [AddCommMonoid A₁] [Module A A₁] [AddCommMonoid E₁] [Module A E₁] (u : A₁ →ₗ[A] E₁) (C : Type u_5) [AddCommMonoid C] [Module A C] (φ : Module.Dual A (A₁ × C)) : (compFstEquiv u C) ((mk (u ∘ₗ LinearMap.fst A A₁ C)) φ) = ((mk u) (φ ∘ₗ LinearMap.inl A A₁ C), φ ∘ₗ LinearMap.inr A A₁ C)

The equivalence compFstEquiv restricts a representative to the two summands.

@[simp]

theorem TauCeti.AuslanderReitenTranspose.compFstEquiv_symm_mk {A : Type u} [Ring A] {A₁ : Type u_1} {E₁ : Type u_3} [AddCommMonoid A₁] [Module A A₁] [AddCommMonoid E₁] [Module A E₁] (u : A₁ →ₗ[A] E₁) (C : Type u_5) [AddCommMonoid C] [Module A C] (φ : Module.Dual A A₁) (ψ : Module.Dual A C) : (compFstEquiv u C).symm ((mk u) φ, ψ) = (mk (u ∘ₗ LinearMap.fst A A₁ C)) (LinearMap.coprod φ ψ)

The inverse of compFstEquiv combines representatives using the canonical functional on the product.

theorem TauCeti.AuslanderReitenTranspose.subsingleton_of_comp_eq_id {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) {r : P₀ →ₗ[A] P₁} (hr : r ∘ₗ p₁ = LinearMap.id) : Subsingleton (AuslanderReitenTranspose p₁)

A split presenting map has vanishing transpose. If p₁ admits a retraction, its Auslander--Reiten transpose is a subsingleton.

No finiteness or projectivity is needed for this direction; TauCeti.AuslanderReitenTranspose.exists_comp_eq_id_of_subsingleton is the converse, and it needs both.

theorem TauCeti.AuslanderReitenTranspose.exists_comp_eq_id_of_subsingleton {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) [Module.Finite A P₁] [Module.Projective A P₁] (h : Subsingleton (AuslanderReitenTranspose p₁)) : ∃ (r : P₀ →ₗ[A] P₁), r ∘ₗ p₁ = LinearMap.id

A vanishing transpose splits the presenting map. If P₁ is a finitely generated projective module and the transpose of p₁ : P₁ → P₀ vanishes, then p₁ admits a retraction.

Both hypotheses on P₁ are needed, and they are needed together: they supply a finite dual basis of P₁, and only finitely many functionals may be assembled into a single map P₀ → P₁.

theorem TauCeti.AuslanderReitenTranspose.subsingleton_iff_exists_comp_eq_id {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) [Module.Finite A P₁] [Module.Projective A P₁] : Subsingleton (AuslanderReitenTranspose p₁) ↔ ∃ (r : P₀ →ₗ[A] P₁), r ∘ₗ p₁ = LinearMap.id

The transpose vanishes exactly when the presenting map splits, for a finitely generated projective P₁.

def TauCeti.AuslanderReitenTranspose.linearEquiv {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] {p₁ : P₁ →ₗ[A] P₀} {Q₀ : Type v'} {Q₁ : Type w'} [AddCommMonoid Q₀] [Module A Q₀] [AddCommMonoid Q₁] [Module A Q₁] {q₁ : Q₁ →ₗ[A] Q₀} (e₀ : P₀ ≃ₗ[A] Q₀) (e₁ : P₁ ≃ₗ[A] Q₁) (hsquare : ↑e₀ ∘ₗ p₁ = q₁ ∘ₗ ↑e₁) : AuslanderReitenTranspose p₁ ≃ₗ[Aᵐᵒᵖ] AuslanderReitenTranspose q₁

An isomorphism of the first square of two projective presentations induces an equivalence of their Auslander--Reiten transposes. On representatives it sends φ : Hom_A(P₁, A) to φ ∘ e₁⁻¹ : Hom_A(Q₁, A).

The equivalence depends only on the two presentation isomorphisms and their commutative square; the maps from P₀ and Q₀ to the presented module do not enter the cokernel.

Equations

• TauCeti.AuslanderReitenTranspose.linearEquiv e₀ e₁ hsquare = TauCeti.AuslanderReitenTranspose.quotientEquiv p₁ (LinearMap.lcomp Aᵐᵒᵖ A q₁).range (LinearEquiv.congrLeft A Aᵐᵒᵖ e₁) ⋯

@[simp]

theorem TauCeti.AuslanderReitenTranspose.linearEquiv_mk {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] {p₁ : P₁ →ₗ[A] P₀} {Q₀ : Type v'} {Q₁ : Type w'} [AddCommMonoid Q₀] [Module A Q₀] [AddCommMonoid Q₁] [Module A Q₁] {q₁ : Q₁ →ₗ[A] Q₀} (e₀ : P₀ ≃ₗ[A] Q₀) (e₁ : P₁ ≃ₗ[A] Q₁) (hsquare : ↑e₀ ∘ₗ p₁ = q₁ ∘ₗ ↑e₁) (φ : Module.Dual A P₁) : (linearEquiv e₀ e₁ hsquare) ((mk p₁) φ) = (mk q₁) ((LinearMap.lcomp Aᵐᵒᵖ A ↑e₁.symm) φ)

The presentation equivalence on transposes, evaluated on a functional representative.

@[simp]

theorem TauCeti.AuslanderReitenTranspose.linearEquiv_refl {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] {p₁ : P₁ →ₗ[A] P₀} : linearEquiv (LinearEquiv.refl A P₀) (LinearEquiv.refl A P₁) ⋯ = LinearEquiv.refl Aᵐᵒᵖ (AuslanderReitenTranspose p₁)

Transport along the identity presentation equivalences is the identity.

@[simp]

theorem TauCeti.AuslanderReitenTranspose.linearEquiv_trans {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] {p₁ : P₁ →ₗ[A] P₀} {Q₀ : Type v'} {Q₁ : Type w'} [AddCommMonoid Q₀] [Module A Q₀] [AddCommMonoid Q₁] [Module A Q₁] {q₁ : Q₁ →ₗ[A] Q₀} {R₀ : Type u_1} {R₁ : Type u_2} [AddCommMonoid R₀] [Module A R₀] [AddCommMonoid R₁] [Module A R₁] {r₁ : R₁ →ₗ[A] R₀} (e₀ : P₀ ≃ₗ[A] Q₀) (e₁ : P₁ ≃ₗ[A] Q₁) (f₀ : Q₀ ≃ₗ[A] R₀) (f₁ : Q₁ ≃ₗ[A] R₁) (he : ↑e₀ ∘ₗ p₁ = q₁ ∘ₗ ↑e₁) (hf : ↑f₀ ∘ₗ q₁ = r₁ ∘ₗ ↑f₁) : linearEquiv e₀ e₁ he ≪≫ₗ linearEquiv f₀ f₁ hf = linearEquiv (e₀ ≪≫ₗ f₀) (e₁ ≪≫ₗ f₁) ⋯

Transport along a composite of presentation equivalences is the composite transport.

@[simp]

theorem TauCeti.AuslanderReitenTranspose.linearEquiv_symm {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] {p₁ : P₁ →ₗ[A] P₀} {Q₀ : Type v'} {Q₁ : Type w'} [AddCommMonoid Q₀] [Module A Q₀] [AddCommMonoid Q₁] [Module A Q₁] {q₁ : Q₁ →ₗ[A] Q₀} (e₀ : P₀ ≃ₗ[A] Q₀) (e₁ : P₁ ≃ₗ[A] Q₁) (hsquare : ↑e₀ ∘ₗ p₁ = q₁ ∘ₗ ↑e₁) : (linearEquiv e₀ e₁ hsquare).symm = linearEquiv e₀.symm e₁.symm ⋯

The inverse of transport is transport along the inverse presentation equivalences.

theorem TauCeti.IsMinimalProjectivePresentation.subsingleton_auslanderReitenTranspose_of_projective {A : Type u} [Ring A] {M : Type u_1} [AddCommGroup M] [Module A M] {P₀ : Type v} [AddCommGroup P₀] [Module A P₀] {P₁ : Type w} [AddCommMonoid P₁] [Module A P₁] {p₁ : P₁ →ₗ[A] P₀} {p₀ : P₀ →ₗ[A] M} [Module.Projective A M] (h : IsMinimalProjectivePresentation p₁ p₀) : Subsingleton (AuslanderReitenTranspose p₁)

The Auslander--Reiten transpose of a projective module is zero, represented here by the stronger typeclass-friendly statement that its underlying quotient is a subsingleton.

theorem TauCeti.IsMinimalProjectivePresentation.projective_of_subsingleton_auslanderReitenTranspose {A : Type u} [Ring A] {M : Type u_1} [AddCommGroup M] [Module A M] {P₀ : Type v} [AddCommGroup P₀] [Module A P₀] {P₁ : Type w} [AddCommGroup P₁] [Module A P₁] {p₁ : P₁ →ₗ[A] P₀} {p₀ : P₀ →ₗ[A] M} [Module.Finite A P₁] (h : IsMinimalProjectivePresentation p₁ p₀) (hTr : Subsingleton (AuslanderReitenTranspose p₁)) : Module.Projective A M

A module with vanishing Auslander--Reiten transpose is projective, the converse of TauCeti.IsMinimalProjectivePresentation.subsingleton_auslanderReitenTranspose_of_projective.

Finite generation of P₁ is a genuine hypothesis rather than a convenience: it is what makes the dual basis splitting p₁ finite. It is automatic for a finitely generated M over an Artin algebra, where such an M has a minimal projective presentation by finitely generated projectives.

theorem TauCeti.IsMinimalProjectivePresentation.subsingleton_auslanderReitenTranspose_iff_projective {A : Type u} [Ring A] {M : Type u_1} [AddCommGroup M] [Module A M] {P₀ : Type v} [AddCommGroup P₀] [Module A P₀] {P₁ : Type w} [AddCommGroup P₁] [Module A P₁] {p₁ : P₁ →ₗ[A] P₀} {p₀ : P₀ →ₗ[A] M} [Module.Finite A P₁] (h : IsMinimalProjectivePresentation p₁ p₀) : Subsingleton (AuslanderReitenTranspose p₁) ↔ Module.Projective A M

The Auslander--Reiten transpose vanishes exactly on the projective modules. This is what makes Tr, and with it the translate τ = D Tr, a construction on non-projective modules: it carries no information about a projective one and detects every other.

theorem TauCeti.IsMinimalProjectivePresentation.nonempty_linearEquiv_auslanderReitenTranspose {A : Type u} [Ring A] {M : Type u_1} [AddCommGroup M] [Module A M] {P₀ : Type v} [AddCommGroup P₀] [Module A P₀] {P₁ : Type w} [AddCommGroup P₁] [Module A P₁] {p₁ : P₁ →ₗ[A] P₀} {p₀ : P₀ →ₗ[A] M} {Q₀ : Type v'} {Q₁ : Type w'} [AddCommGroup Q₀] [Module A Q₀] [AddCommGroup Q₁] [Module A Q₁] {q₁ : Q₁ →ₗ[A] Q₀} {q₀ : Q₀ →ₗ[A] M} (h : IsMinimalProjectivePresentation p₁ p₀) (h' : IsMinimalProjectivePresentation q₁ q₀) : Nonempty (AuslanderReitenTranspose p₁ ≃ₗ[Aᵐᵒᵖ] AuslanderReitenTranspose q₁)

The Auslander--Reiten transpose is independent, up to opposite-linear equivalence, of the chosen minimal projective presentation of a module.