Recovering module equivalences from scalar duals #
An equivalence between the left scalar duals of two reflexive right modules gives an equivalence of the original right modules in the opposite direction. The dual actions are specified by equivariant pairings, avoiding competing global module instances on duals. This lets constructions involving scalar duality recover actual module isomorphism classes.
The construction uses Mathlib's Module.evalEquiv and LinearEquiv.dualMap; the
equivariant pairing interface follows LinearEquiv.dualEndRingEquiv.
References #
- M. Auslander, I. Reiten, S. Smalø, Representation Theory of Artin Algebras, Cambridge University Press (1995), Section I.3.
noncomputable def
LinearEquiv.ofEquivariantDual
{k : Type u}
[CommSemiring k]
{A : Type v}
[Semiring A]
[Algebra k A]
{N₁ : Type w₁}
{N₂ : Type w₂}
[AddCommMonoid N₁]
[Module Aᵐᵒᵖ N₁]
[Module k N₁]
[IsScalarTower k Aᵐᵒᵖ N₁]
[AddCommMonoid N₂]
[Module Aᵐᵒᵖ N₂]
[Module k N₂]
[IsScalarTower k Aᵐᵒᵖ N₂]
[Module.IsReflexive k N₁]
[Module.IsReflexive k N₂]
{Q₁ : Type z₁}
{Q₂ : Type z₂}
[AddCommMonoid Q₁]
[Module A Q₁]
[Module k Q₁]
[AddCommMonoid Q₂]
[Module A Q₂]
[Module k Q₂]
(e₁ : Q₁ ≃ₗ[k] Module.Dual k N₁)
(e₂ : Q₂ ≃ₗ[k] Module.Dual k N₂)
(h₁ : ∀ (a : A) (q : Q₁) (x : N₁), (e₁ (a • q)) x = (e₁ q) (MulOpposite.op a • x))
(h₂ : ∀ (a : A) (q : Q₂) (x : N₂), (e₂ (a • q)) x = (e₂ q) (MulOpposite.op a • x))
(f : Q₁ ≃ₗ[A] Q₂)
:
An equivalence of equivariantly identified scalar duals recovers a right-module equivalence in the reverse direction, provided both original modules are reflexive.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LinearEquiv.ofEquivariantDual_apply_apply
{k : Type u}
[CommSemiring k]
{A : Type v}
[Semiring A]
[Algebra k A]
{N₁ : Type w₁}
{N₂ : Type w₂}
[AddCommMonoid N₁]
[Module Aᵐᵒᵖ N₁]
[Module k N₁]
[IsScalarTower k Aᵐᵒᵖ N₁]
[AddCommMonoid N₂]
[Module Aᵐᵒᵖ N₂]
[Module k N₂]
[IsScalarTower k Aᵐᵒᵖ N₂]
[Module.IsReflexive k N₁]
[Module.IsReflexive k N₂]
{Q₁ : Type z₁}
{Q₂ : Type z₂}
[AddCommMonoid Q₁]
[Module A Q₁]
[Module k Q₁]
[AddCommMonoid Q₂]
[Module A Q₂]
[Module k Q₂]
(e₁ : Q₁ ≃ₗ[k] Module.Dual k N₁)
(e₂ : Q₂ ≃ₗ[k] Module.Dual k N₂)
(h₁ : ∀ (a : A) (q : Q₁) (x : N₁), (e₁ (a • q)) x = (e₁ q) (MulOpposite.op a • x))
(h₂ : ∀ (a : A) (q : Q₂) (x : N₂), (e₂ (a • q)) x = (e₂ q) (MulOpposite.op a • x))
(f : Q₁ ≃ₗ[A] Q₂)
(q : Q₁)
(x : N₂)
:
The recovered equivalence moves the given equivalence across the evaluation pairing.