Commit 2022-11-18 10:49 19a70dce

View on Github →

feat(algebra/category/FinVect): generalize to fgModule (#13962) Generalize the category FinVect of finite dimensional vector spaces to fgModule, the category of finitely generated modules.

Estimated changes

Deleted src/algebra/category/FinVect.lean

deleted def FinVect.FinVect_coevaluation

deleted theorem FinVect.FinVect_coevaluation_apply_one

deleted def FinVect.FinVect_dual

deleted def FinVect.FinVect_evaluation

deleted theorem FinVect.FinVect_evaluation_apply

deleted def FinVect.forget₂_monoidal

deleted theorem FinVect.ihom_obj

deleted theorem FinVect.iso.conj_eq_conj

deleted def FinVect.iso_to_linear_equiv

deleted def FinVect.of

deleted def FinVect

deleted def linear_equiv.to_FinVect_iso

Created src/algebra/category/fgModule/basic.lean

added def fgModule.fgModule_coevaluation

added theorem fgModule.fgModule_coevaluation_apply_one

added def fgModule.fgModule_dual

added def fgModule.fgModule_evaluation

added theorem fgModule.fgModule_evaluation_apply

added def fgModule.forget₂_monoidal

added theorem fgModule.ihom_obj

added theorem fgModule.iso.conj_eq_conj

added def fgModule.iso_to_linear_equiv

added def fgModule.of

added def fgModule

added def linear_equiv.to_fgModule_iso

Renamed src/algebra/category/FinVect/limits.lean to src/algebra/category/fgModule/limits.lean

deleted def FinVect.forget₂_creates_limit

added def fgModule.forget₂_creates_limit

Modified src/representation_theory/fdRep.lean