English
For a finite family of subspaces W_i of V, the dual annihilator of the infimum (intersection) equals the supremum (sum) of the dual annihilators:
Русский
Для конечного семейства подпространств W_i ⊆ V дуальный аннигилятор пересечения равен сумме дуальных аннигиляторов.
LaTeX
$$(⋂ i, W_i)^{\\perp} = ⋁ i, W_i^{\\perp}$$
Lean4
theorem dualAnnihilator_inf_eq (W W' : Subspace K V₁) :
(W ⊓ W').dualAnnihilator = W.dualAnnihilator ⊔ W'.dualAnnihilator :=
by
refine le_antisymm ?_ (sup_dualAnnihilator_le_inf W W')
let F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (Submodule.mkQ W).prod (Submodule.mkQ W')
have : LinearMap.ker F = W ⊓ W' := by simp only [F, LinearMap.ker_prod, ker_mkQ]
rw [← this, ← LinearMap.range_dualMap_eq_dualAnnihilator_ker]
intro φ
rw [LinearMap.mem_range]
rintro ⟨x, rfl⟩
rw [Submodule.mem_sup]
obtain ⟨⟨a, b⟩, rfl⟩ := (dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W')).surjective x
obtain ⟨a', rfl⟩ := (dualQuotEquivDualAnnihilator W).symm.surjective a
obtain ⟨b', rfl⟩ := (dualQuotEquivDualAnnihilator W').symm.surjective b
use a', a'.property, b', b'.property
rfl
-- This is also true if `V₁` is finite dimensional since one can restrict `ι` to some subtype
-- for which the infimum and supremum are the same.
-- The obstruction to the `dualAnnihilator_inf_eq` argument carrying through is that we need
-- for `Module.Dual R (Π (i : ι), V ⧸ W i) ≃ₗ[K] Π (i : ι), Module.Dual R (V ⧸ W i)`, which is not
-- true for infinite `ι`. One would need to add additional hypothesis on `W` (for example, it might
-- be true when the family is inf-closed).
-- TODO: generalize to `Sort`
