English
A definitional linear equivalence linking duals of quotients to quotients of duals via a chosen splitting, for finite-dimensional spaces.
Русский
Определение линейного эквивалента между дуальными тождествами фактор-пространств и факторными дуальными пространствами через заданное разложение.
LaTeX
$$$W\\,\\text{dualQuotDistrib} : \\mathrm{Dual}(V/W) \\simeq \\mathrm{Dual}(V) / \\mathrm{range}(W.dualLift)$$$
Lean4
/-- For finite-dimensional vector spaces, one can distribute duals over quotients by identifying
`W.dualLift.range` with `W`. Note that this depends on a choice of splitting of `V₁`. -/
def dualQuotDistrib [FiniteDimensional K V₁] (W : Subspace K V₁) :
Module.Dual K (V₁ ⧸ W) ≃ₗ[K] Module.Dual K V₁ ⧸ LinearMap.range W.dualLift :=
W.dualQuotEquivDualAnnihilator.trans W.quotDualEquivAnnihilator.symm
