English
The dual of the top submodule equals the top submodule when A is (IsField) or more generally determined by the surjectivity of the trace; otherwise it equals the bottom.
Русский
Дуальность по следу верхнего подмодуля равна верхнему подмодулю, если A удовлетворяет условиям, иначе равна нижнему.
LaTeX
$$traceDual_top = top if IsField A else bottom$$
Lean4
theorem traceDual_top' :
(⊤ : Submodule B L)ᵛ = if ((LinearMap.range (Algebra.trace K L)).restrictScalars A ≤ 1) then ⊤ else ⊥ := by
classical
split_ifs with h
· rw [_root_.eq_top_iff]
exact fun _ _ _ _ ↦ h ⟨_, rfl⟩
· simp only [SetLike.le_def, restrictScalars_mem, LinearMap.mem_range, mem_one, forall_exists_index,
forall_apply_eq_imp_iff, not_forall, not_exists] at h
obtain ⟨b, hb⟩ := h
simp_rw [eq_bot_iff, SetLike.le_def, mem_bot, mem_traceDual, mem_top, true_implies, traceForm_apply,
RingHom.mem_range]
contrapose! hb with hx'
obtain ⟨c, hc, hc0⟩ := hx'
simpa [hc0] using hc (c⁻¹ * b)
