English
Under AKLB setting, traceDual A K I defines the submodule of B L consisting of elements x such that Tr(x, y) ∈ A for all y ∈ I.
Русский
В настройке AKLB traceDual A K I задаёт подмодуля B L, состоящего из элементов x, для которых Tr(x, y) ∈ A для всех y ∈ I.
LaTeX
$$traceDual (I : Submodule B L) : Submodule B L$$
Lean4
/-- Under the AKLB setting, `Iᵛ := traceDual A K (I : Submodule B L)` is the
`Submodule B L` such that `x ∈ Iᵛ ↔ ∀ y ∈ I, Tr(x, y) ∈ A` -/
noncomputable def traceDual (I : Submodule B L) : Submodule B L
where
__ := (traceForm K L).dualSubmodule (I.restrictScalars A)
smul_mem' c x hx a
ha := by
rw [traceForm_apply, smul_mul_assoc, mul_comm, ← smul_mul_assoc, mul_comm]
exact hx _ (Submodule.smul_mem _ c ha)
