1. Physlib
  2. Mathematics
  3. ConjModule
Imports
/- Copyright (c) 2026 Andrea Pari. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Andrea Pari -/ module public import Mathlib.Algebra.Module.Equiv.Defs public import Mathlib.Algebra.Star.Module public import Mathlib.LinearAlgebra.Basis.Defs public import Mathlib.Tactic.Ring

The conjugate module

Over a commutative star-ring k, the conjugate module ConjModule M of a k-module M is the same additive group with the scalar action twisted by conjugation: r • v := star r • v. It turns a sesquilinear pairing into a bilinear one: a map conjugate-linear in a slot M is linear in the slot ConjModule M.

ConjModule M is a type synonym carrying a fresh Module k instance (Module.compHom along starRingEnd k), so the twisted action does not leak onto M and vice versa. The canonical conjugate-linear identity conjEquiv : M ≃ₛₗ[starRingEnd k] ConjModule M, the involution ConjModule (ConjModule M) ≃ₗ[k] M, and the transported basis Basis.conj are provided.

Key results

    ConjModule : the conjugate-module type synonym, with its twisted Module instance.

    conjEquiv : the canonical conjugate-linear equivalence M ≃ₛₗ[starRingEnd k] ConjModule M.

    ConjModule.involution : the involution ConjModule (ConjModule M) ≃ₗ[k] M.

    Basis.conj : a basis of M transported to a basis of ConjModule M (coordinates by star).

@[expose] public section

The conjugate module of M: the same additive group with the scalar action twisted by conjugation, r • v = star r • v. A type synonym so the twisted action stays off M.

def ConjModule (M : Type*) := M
instance : AddCommGroup (ConjModule M) := inferInstanceAs (AddCommGroup M)

The twisted action r • v = star r • v, obtained by restricting scalars along the conjugation ring endomorphism starRingEnd k.

instance instModule : Module k (ConjModule M) := Module.compHom M (starRingEnd k)

The canonical conjugate-linear equivalence M ≃ₛₗ[starRingEnd k] ConjModule M, the identity on the underlying additive group.

All goals completed! 🐙 invFun v := v left_inv _ := rfl right_inv _ := rfl

Conjugating twice returns the original module: the k-linear isomorphism ConjModule (ConjModule M) ≃ₗ[k] M. It is k-linear, not merely semilinear, because starRingEnd k composed with itself is the identity.

def involution : ConjModule (ConjModule M) ≃ₗ[k] M := ((conjEquiv (k := k) (M := M)).trans (conjEquiv (k := k) (M := ConjModule M))).symm

Coordinates in Basis.conj b are the star of the coordinates in b.

@[simp] lemma _root_.Basis.conj_repr_apply (b : Basis ι k M) (v : ConjModule M) (i : ι) : (Basis.conj b).repr v i = star (b.repr ((conjEquiv (k := k) (M := M)).symm v) i) := rfl

The basis vectors of Basis.conj b are those of b, viewed through conjEquiv.

@[simp] lemma _root_.Basis.conj_apply (b : Basis ι k M) (i : ι) : Basis.conj b i = conjEquiv (k := k) (M := M) (b i) := k:Type u_1inst✝³:CommRing kinst✝²:StarRing kM:Type u_2inst✝¹:AddCommGroup Minst✝:Module k Mι:Type u_3b:Basis ι k Mi:ι⊢ (Basis.conj b) i = conjEquiv (b i) k:Type u_1inst✝³:CommRing kinst✝²:StarRing kM:Type u_2inst✝¹:AddCommGroup Minst✝:Module k Mι:Type u_3b:Basis ι k Mi:ι⊢ (Basis.conj b).repr ((Basis.conj b) i) = (Basis.conj b).repr (conjEquiv (b i)) k:Type u_1inst✝³:CommRing kinst✝²:StarRing kM:Type u_2inst✝¹:AddCommGroup Minst✝:Module k Mι:Type u_3b:Basis ι k Mi:ιj:ι⊢ ((Basis.conj b).repr ((Basis.conj b) i)) j = ((Basis.conj b).repr (conjEquiv (b i))) j k:Type u_1inst✝³:CommRing kinst✝²:StarRing kM:Type u_2inst✝¹:AddCommGroup Minst✝:Module k Mι:Type u_3b:Basis ι k Mi:ιj:ιh:j = i⊢ ((Basis.conj b).repr ((Basis.conj b) i)) j = ((Basis.conj b).repr (conjEquiv (b i))) jk:Type u_1inst✝³:CommRing kinst✝²:StarRing kM:Type u_2inst✝¹:AddCommGroup Minst✝:Module k Mι:Type u_3b:Basis ι k Mi:ιj:ιh:j ≠ i⊢ ((Basis.conj b).repr ((Basis.conj b) i)) j = ((Basis.conj b).repr (conjEquiv (b i))) j k:Type u_1inst✝³:CommRing kinst✝²:StarRing kM:Type u_2inst✝¹:AddCommGroup Minst✝:Module k Mι:Type u_3b:Basis ι k Mi:ιj:ιh:j = i⊢ ((Basis.conj b).repr ((Basis.conj b) i)) j = ((Basis.conj b).repr (conjEquiv (b i))) j k:Type u_1inst✝³:CommRing kinst✝²:StarRing kM:Type u_2inst✝¹:AddCommGroup Minst✝:Module k Mι:Type u_3b:Basis ι k Mj:ι⊢ ((Basis.conj b).repr ((Basis.conj b) j)) j = ((Basis.conj b).repr (conjEquiv (b j))) j; All goals completed! 🐙 k:Type u_1inst✝³:CommRing kinst✝²:StarRing kM:Type u_2inst✝¹:AddCommGroup Minst✝:Module k Mι:Type u_3b:Basis ι k Mi:ιj:ιh:j ≠ i⊢ ((Basis.conj b).repr ((Basis.conj b) i)) j = ((Basis.conj b).repr (conjEquiv (b i))) j All goals completed! 🐙