[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
inst✝¹ : Finite R M
inst✝ : Finite R N
⊢ Free R (M →ₗ[R] N)
[PROOFSTEP]
cases subsingleton_or_nontrivial R
[GOAL]
case inl
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
inst✝¹ : Finite R M
inst✝ : Finite R N
h✝ : Subsingleton R
⊢ Free R (M →ₗ[R] N)
[PROOFSTEP]
apply Module.Free.of_subsingleton'
[GOAL]
case inr
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
inst✝¹ : Finite R M
inst✝ : Finite R N
h✝ : Nontrivial R
⊢ Free R (M →ₗ[R] N)
[PROOFSTEP]
classical exact Module.Free.of_equiv (LinearMap.toMatrix (chooseBasis R M) (chooseBasis R N)).symm
[GOAL]
case inr
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
inst✝¹ : Finite R M
inst✝ : Finite R N
h✝ : Nontrivial R
⊢ Free R (M →ₗ[R] N)
[PROOFSTEP]
exact Module.Free.of_equiv (LinearMap.toMatrix (chooseBasis R M) (chooseBasis R N)).symm
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
inst✝¹ : Finite R M
inst✝ : Finite R N
⊢ Finite R (M →ₗ[R] N)
[PROOFSTEP]
cases subsingleton_or_nontrivial R
[GOAL]
case inl
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
inst✝¹ : Finite R M
inst✝ : Finite R N
h✝ : Subsingleton R
⊢ Finite R (M →ₗ[R] N)
[PROOFSTEP]
infer_instance
[GOAL]
case inr
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
inst✝¹ : Finite R M
inst✝ : Finite R N
h✝ : Nontrivial R
⊢ Finite R (M →ₗ[R] N)
[PROOFSTEP]
classical
have f := (LinearMap.toMatrix (chooseBasis R M) (chooseBasis R N)).symm
exact Module.Finite.of_surjective f.toLinearMap (LinearEquiv.surjective f)
[GOAL]
case inr
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
inst✝¹ : Finite R M
inst✝ : Finite R N
h✝ : Nontrivial R
⊢ Finite R (M →ₗ[R] N)
[PROOFSTEP]
have f := (LinearMap.toMatrix (chooseBasis R M) (chooseBasis R N)).symm
[GOAL]
case inr
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
inst✝¹ : Finite R M
inst✝ : Finite R N
h✝ : Nontrivial R
f : Matrix (Free.ChooseBasisIndex R N) (Free.ChooseBasisIndex R M) R ≃ₗ[R] M →ₗ[R] N
⊢ Finite R (M →ₗ[R] N)
[PROOFSTEP]
exact Module.Finite.of_surjective f.toLinearMap (LinearEquiv.surjective f)
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁹ : CommRing R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Free R N
inst✝ : Module.Finite R N
⊢ finrank R (M →ₗ[R] N) = finrank R M * finrank R N
[PROOFSTEP]
classical
letI := nontrivial_of_invariantBasisNumber R
have h := LinearMap.toMatrix (chooseBasis R M) (chooseBasis R N)
simp_rw [h.finrank_eq, FiniteDimensional.finrank_matrix, FiniteDimensional.finrank_eq_card_chooseBasisIndex, mul_comm]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁹ : CommRing R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Free R N
inst✝ : Module.Finite R N
⊢ finrank R (M →ₗ[R] N) = finrank R M * finrank R N
[PROOFSTEP]
letI := nontrivial_of_invariantBasisNumber R
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁹ : CommRing R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Free R N
inst✝ : Module.Finite R N
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
⊢ finrank R (M →ₗ[R] N) = finrank R M * finrank R N
[PROOFSTEP]
have h := LinearMap.toMatrix (chooseBasis R M) (chooseBasis R N)
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁹ : CommRing R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Free R N
inst✝ : Module.Finite R N
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
h : (M →ₗ[R] N) ≃ₗ[R] Matrix (Module.Free.ChooseBasisIndex R N) (Module.Free.ChooseBasisIndex R M) R
⊢ finrank R (M →ₗ[R] N) = finrank R M * finrank R N
[PROOFSTEP]
simp_rw [h.finrank_eq, FiniteDimensional.finrank_matrix, FiniteDimensional.finrank_eq_card_chooseBasisIndex, mul_comm]
[GOAL]
R : Type u
M : Type v
N : Type w
K m n : Type u
inst✝³ : CommRing K
inst✝² : StrongRankCondition K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
⊢ LinearMap.rank (↑toLin' (vecMulVec w v)) ≤ 1
[PROOFSTEP]
rw [Matrix.vecMulVec_eq, Matrix.toLin'_mul]
[GOAL]
R : Type u
M : Type v
N : Type w
K m n : Type u
inst✝³ : CommRing K
inst✝² : StrongRankCondition K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
⊢ LinearMap.rank (LinearMap.comp (↑toLin' (col w)) (↑toLin' (row v))) ≤ 1
[PROOFSTEP]
refine' le_trans (LinearMap.rank_comp_le_left _ _) _
[GOAL]
R : Type u
M : Type v
N : Type w
K m n : Type u
inst✝³ : CommRing K
inst✝² : StrongRankCondition K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
⊢ LinearMap.rank (↑toLin' (col w)) ≤ 1
[PROOFSTEP]
refine' (LinearMap.rank_le_domain _).trans_eq _
[GOAL]
R : Type u
M : Type v
N : Type w
K m n : Type u
inst✝³ : CommRing K
inst✝² : StrongRankCondition K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
⊢ Module.rank K (Unit → K) = 1
[PROOFSTEP]
rw [rank_fun', Fintype.card_unit, Nat.cast_one]
