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₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K (V₂ ⧸ range f) + finrank K { x // x ∈ range f } = finrank K V₂
⊢ finrank K { x // x ∈ range (dualMap f) } = finrank K { x // x ∈ range f }
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₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
⊢ finrank K { x // x ∈ range (dualMap f) } = finrank K { x // x ∈ range f }
have that := Submodule.finrank_quotient_add_finrank (LinearMap.range f)
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₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K (V₂ ⧸ range f) + finrank K { x // x ∈ range f } = finrank K V₂
equiv : (V₂ ⧸ range f) ≃ₗ[K] { x // x ∈ Submodule.dualAnnihilator (range f) } := Subspace.quotEquivAnnihilator (range f)
⊢ finrank K { x // x ∈ range (dualMap f) } = finrank K { x // x ∈ range f }
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₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K (V₂ ⧸ range f) + finrank K { x // x ∈ range f } = finrank K V₂
⊢ finrank K { x // x ∈ range (dualMap f) } = finrank K { x // x ∈ range f }
let equiv := (Subspace.quotEquivAnnihilator <| LinearMap.range f)
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₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K (V₂ ⧸ range f) + finrank K { x // x ∈ range f } = finrank K V₂
equiv : (V₂ ⧸ range f) ≃ₗ[K] { x // x ∈ Submodule.dualAnnihilator (range f) } := Subspace.quotEquivAnnihilator (range f)
eq : finrank K (V₂ ⧸ range f) = finrank K { x // x ∈ Submodule.dualAnnihilator (range f) }
⊢ finrank K { x // x ∈ range (dualMap f) } = finrank K { x // x ∈ range f }
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₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K (V₂ ⧸ range f) + finrank K { x // x ∈ range f } = finrank K V₂
equiv : (V₂ ⧸ range f) ≃ₗ[K] { x // x ∈ Submodule.dualAnnihilator (range f) } := Subspace.quotEquivAnnihilator (range f)
⊢ finrank K { x // x ∈ range (dualMap f) } = finrank K { x // x ∈ range f }
have eq := LinearEquiv.finrank_eq (R := K) (M := (V₂ ⧸ range f))
  (M₂ := { x // x ∈ Submodule.dualAnnihilator (range f) }) equiv
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₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K { x // x ∈ ker (dualMap f) } + finrank K { x // x ∈ range f } = finrank K V₂
equiv : (V₂ ⧸ range f) ≃ₗ[K] { x // x ∈ Submodule.dualAnnihilator (range f) } := Subspace.quotEquivAnnihilator (range f)
eq : finrank K (V₂ ⧸ range f) = finrank K { x // x ∈ Submodule.dualAnnihilator (range f) }
⊢ finrank K { x // x ∈ range (dualMap f) } = finrank K { x // x ∈ range f }
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₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K (V₂ ⧸ range f) + finrank K { x // x ∈ range f } = finrank K V₂
equiv : (V₂ ⧸ range f) ≃ₗ[K] { x // x ∈ Submodule.dualAnnihilator (range f) } := Subspace.quotEquivAnnihilator (range f)
eq : finrank K (V₂ ⧸ range f) = finrank K { x // x ∈ Submodule.dualAnnihilator (range f) }
⊢ finrank K { x // x ∈ range (dualMap f) } = finrank K { x // x ∈ range f }
rw [eq, ←ker_dualMap_eq_dualAnnihilator_range] at that
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₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K { x // x ∈ ker (dualMap f) } + finrank K { x // x ∈ range f } = finrank K (Dual K V₂)
equiv : (V₂ ⧸ range f) ≃ₗ[K] { x // x ∈ Submodule.dualAnnihilator (range f) } := Subspace.quotEquivAnnihilator (range f)
eq : finrank K (V₂ ⧸ range f) = finrank K { x // x ∈ Submodule.dualAnnihilator (range f) }
⊢ finrank K { x // x ∈ range (dualMap f) } = finrank K { x // x ∈ range f }
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₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K { x // x ∈ ker (dualMap f) } + finrank K { x // x ∈ range f } = finrank K V₂
equiv : (V₂ ⧸ range f) ≃ₗ[K] { x // x ∈ Submodule.dualAnnihilator (range f) } := Subspace.quotEquivAnnihilator (range f)
eq : finrank K (V₂ ⧸ range f) = finrank K { x // x ∈ Submodule.dualAnnihilator (range f) }
⊢ finrank K { x // x ∈ range (dualMap f) } = finrank K { x // x ∈ range f }
conv_rhs at that => rw [← Subspace.dual_finrank_eq]
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₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K { x // x ∈ ker (dualMap f) } + finrank K { x // x ∈ range f } = finrank K (Dual K V₂)
equiv : (V₂ ⧸ range f) ≃ₗ[K] { x // x ∈ Submodule.dualAnnihilator (range f) } := Subspace.quotEquivAnnihilator (range f)
eq : finrank K (V₂ ⧸ range f) = finrank K { x // x ∈ Submodule.dualAnnihilator (range f) }
⊢ (fun x => x + finrank K { x // x ∈ ker (dualMap f) }) (finrank K { x // x ∈ range (dualMap f) }) =
    (fun x => x + finrank K { x // x ∈ ker (dualMap f) }) (finrank K { x // x ∈ range f })
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₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K { x // x ∈ ker (dualMap f) } + finrank K { x // x ∈ range f } = finrank K (Dual K V₂)
equiv : (V₂ ⧸ range f) ≃ₗ[K] { x // x ∈ Submodule.dualAnnihilator (range f) } := Subspace.quotEquivAnnihilator (range f)
eq : finrank K (V₂ ⧸ range f) = finrank K { x // x ∈ Submodule.dualAnnihilator (range f) }
⊢ finrank K { x // x ∈ range (dualMap f) } = finrank K { x // x ∈ range f }
refine' add_left_injective (finrank K <| LinearMap.ker f.dualMap) _
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₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K { x // x ∈ ker (dualMap f) } + finrank K { x // x ∈ range f } = finrank K (Dual K V₂)
equiv : (V₂ ⧸ range f) ≃ₗ[K] { x // x ∈ Submodule.dualAnnihilator (range f) } := Subspace.quotEquivAnnihilator (range f)
eq : finrank K (V₂ ⧸ range f) = finrank K { x // x ∈ Submodule.dualAnnihilator (range f) }
⊢ finrank K { x // x ∈ range (dualMap f) } + finrank K { x // x ∈ ker (dualMap f) } =
    finrank K { x // x ∈ range f } + finrank K { x // x ∈ ker (dualMap f) }
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₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K { x // x ∈ ker (dualMap f) } + finrank K { x // x ∈ range f } = finrank K (Dual K V₂)
equiv : (V₂ ⧸ range f) ≃ₗ[K] { x // x ∈ Submodule.dualAnnihilator (range f) } := Subspace.quotEquivAnnihilator (range f)
eq : finrank K (V₂ ⧸ range f) = finrank K { x // x ∈ Submodule.dualAnnihilator (range f) }
⊢ (fun x => x + finrank K { x // x ∈ ker (dualMap f) }) (finrank K { x // x ∈ range (dualMap f) }) =
    (fun x => x + finrank K { x // x ∈ ker (dualMap f) }) (finrank K { x // x ∈ range f })
change _ + _ = _ + _
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₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K { x // x ∈ ker (dualMap f) } + finrank K { x // x ∈ range f } = finrank K (Dual K V₂)
equiv : (V₂ ⧸ range f) ≃ₗ[K] { x // x ∈ Submodule.dualAnnihilator (range f) } := Subspace.quotEquivAnnihilator (range f)
eq : finrank K (V₂ ⧸ range f) = finrank K { x // x ∈ Submodule.dualAnnihilator (range f) }
⊢ finrank K { x // x ∈ range (dualMap f) } + finrank K { x // x ∈ ker (dualMap f) } =
    finrank K { x // x ∈ range f } + finrank K { x // x ∈ ker (dualMap f) }
rw [finrank_range_add_finrank_ker f.dualMap, add_comm, that]