K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
⊢ dualAnnihilator (W ⊓ W') = dualAnnihilator W ⊔ dualAnnihilator W'
refine' le_antisymm _ (sup_dualAnnihilator_le_inf W W')
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'
let F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (Submodule.mkQ W).prod (Submodule.mkQ W')
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'
have : LinearMap.ker F = W ⊓ W' := by simp only [LinearMap.ker_prod, ker_mkQ]
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
⊢ LinearMap.range (LinearMap.dualMap F) ≤ dualAnnihilator W ⊔ dualAnnihilator W'
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'
rw [← this, ← LinearMap.range_dualMap_eq_dualAnnihilator_ker]
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
φ : Dual K V₁
⊢ φ ∈ LinearMap.range (LinearMap.dualMap F) → φ ∈ dualAnnihilator W ⊔ dualAnnihilator W'
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
⊢ LinearMap.range (LinearMap.dualMap F) ≤ dualAnnihilator W ⊔ dualAnnihilator W'
intro φ
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
φ : Dual K V₁
⊢ (∃ y, ↑(LinearMap.dualMap F) y = φ) → φ ∈ dualAnnihilator W ⊔ dualAnnihilator W'
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
φ : Dual K V₁
⊢ φ ∈ LinearMap.range (LinearMap.dualMap F) → φ ∈ dualAnnihilator W ⊔ dualAnnihilator W'
rw [LinearMap.mem_range]
case intro
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
x : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')
⊢ ↑(LinearMap.dualMap F) x ∈ dualAnnihilator W ⊔ dualAnnihilator W'
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
φ : Dual K V₁
⊢ (∃ y, ↑(LinearMap.dualMap F) y = φ) → φ ∈ dualAnnihilator W ⊔ dualAnnihilator W'
rintro ⟨x, rfl⟩
case intro
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
x : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')
⊢ ∃ y, y ∈ dualAnnihilator W ∧ ∃ z, z ∈ dualAnnihilator W' ∧ y + z = ↑(LinearMap.dualMap F) x
case intro
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
x : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')
⊢ ↑(LinearMap.dualMap F) x ∈ dualAnnihilator W ⊔ dualAnnihilator W'
rw [Submodule.mem_sup]
case intro.intro.mk
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
a : Dual K (V₁ ⧸ W)
b : Dual K (V₁ ⧸ W')
⊢ ∃ y,
    y ∈ dualAnnihilator W ∧
      ∃ z,
        z ∈ dualAnnihilator W' ∧ y + z = ↑(LinearMap.dualMap F) (↑(dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W')) (a, b))
case intro
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
x : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')
⊢ ∃ y, y ∈ dualAnnihilator W ∧ ∃ z, z ∈ dualAnnihilator W' ∧ y + z = ↑(LinearMap.dualMap F) x
obtain ⟨⟨a, b⟩, rfl⟩ := (dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W')).surjective x
case intro.intro.mk.intro
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
b : Dual K (V₁ ⧸ W')
a' : { x // x ∈ dualAnnihilator W }
⊢ ∃ y,
    y ∈ dualAnnihilator W ∧
      ∃ z,
        z ∈ dualAnnihilator W' ∧
          y + z =
            ↑(LinearMap.dualMap F)
              (↑(dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W'))
                (↑(LinearEquiv.symm (dualQuotEquivDualAnnihilator W)) a', b))
case intro.intro.mk
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
a : Dual K (V₁ ⧸ W)
b : Dual K (V₁ ⧸ W')
⊢ ∃ y,
    y ∈ dualAnnihilator W ∧
      ∃ z,
        z ∈ dualAnnihilator W' ∧ y + z = ↑(LinearMap.dualMap F) (↑(dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W')) (a, b))
obtain ⟨a', rfl⟩ := (dualQuotEquivDualAnnihilator W).symm.surjective a
case intro.intro.mk.intro.intro
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
a' : { x // x ∈ dualAnnihilator W }
b' : { x // x ∈ dualAnnihilator W' }
⊢ ∃ y,
    y ∈ dualAnnihilator W ∧
      ∃ z,
        z ∈ dualAnnihilator W' ∧
          y + z =
            ↑(LinearMap.dualMap F)
              (↑(dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W'))
                (↑(LinearEquiv.symm (dualQuotEquivDualAnnihilator W)) a',
                  ↑(LinearEquiv.symm (dualQuotEquivDualAnnihilator W')) b'))
case intro.intro.mk.intro
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
b : Dual K (V₁ ⧸ W')
a' : { x // x ∈ dualAnnihilator W }
⊢ ∃ y,
    y ∈ dualAnnihilator W ∧
      ∃ z,
        z ∈ dualAnnihilator W' ∧
          y + z =
            ↑(LinearMap.dualMap F)
              (↑(dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W'))
                (↑(LinearEquiv.symm (dualQuotEquivDualAnnihilator W)) a', b))
obtain ⟨b', rfl⟩ := (dualQuotEquivDualAnnihilator W').symm.surjective b
case intro.intro.mk.intro.intro
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
a' : { x // x ∈ dualAnnihilator W }
b' : { x // x ∈ dualAnnihilator W' }
⊢ ↑a' + ↑b' =
    ↑(LinearMap.dualMap F)
      (↑(dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W'))
        (↑(LinearEquiv.symm (dualQuotEquivDualAnnihilator W)) a',
          ↑(LinearEquiv.symm (dualQuotEquivDualAnnihilator W')) b'))
case intro.intro.mk.intro.intro
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
a' : { x // x ∈ dualAnnihilator W }
b' : { x // x ∈ dualAnnihilator W' }
⊢ ∃ y,
    y ∈ dualAnnihilator W ∧
      ∃ z,
        z ∈ dualAnnihilator W' ∧
          y + z =
            ↑(LinearMap.dualMap F)
              (↑(dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W'))
                (↑(LinearEquiv.symm (dualQuotEquivDualAnnihilator W)) a',
                  ↑(LinearEquiv.symm (dualQuotEquivDualAnnihilator W')) b'))
use a', a'.property, b', b'.property
no goals
case intro.intro.mk.intro.intro
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
a' : { x // x ∈ dualAnnihilator W }
b' : { x // x ∈ dualAnnihilator W' }
⊢ ↑a' + ↑b' =
    ↑(LinearMap.dualMap F)
      (↑(dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W'))
        (↑(LinearEquiv.symm (dualQuotEquivDualAnnihilator W)) a',
          ↑(LinearEquiv.symm (dualQuotEquivDualAnnihilator W')) b'))
rfl
no goals
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
⊢ LinearMap.ker F = W ⊓ W'
simp only [LinearMap.ker_prod, ker_mkQ]