Commit 2024-11-14 10:43 4e4d3776

View on Github →

chore(RingTheory): split Finiteness.lean into many smaller files (#18964) This PR splits off RingTheory/Finiteness.lean, where finitely generated (sub)modules are defined, into many different files:

  • RingTheory/Finiteness/Basic.lean: basic properties and instances of Submodule.FG and Module.Finite
  • RingTheory/Finiteness/Bilinear.lean: results involving bilinear maps
  • RingTheory/Finiteness/Cardinality.lean: finite modules and types with finite cardinality
  • RingTheory/Finiteness/Defs.lean: definition of finitely generated (sub)modules and ideals
  • RingTheory/Finiteness/Ideal.lean: results on finitely generated ideals
  • RingTheory/Finiteness/Lattice.lean: finiteness of suprema in the submodule lattice
  • RingTheory/Finiteness/Nakayama.lean: Nakayama's lemma
  • RingTheory/Finiteness/Nilpotent.lean: results on nilpotent maps on finite modules
  • RingTheory/Finiteness/Prod.lean: results involving products of (sub)modules
  • RingTheory/Finiteness/Projectve.lean: results on finite projective modules
  • RingTheory/Finiteness/Finsupp.lean: results involving (D)Finsupp
  • RingTheory/Finiteness/Subalgebra.lean: results involving (sub)algebras
  • RingTheory/Finiteness/TensorProduct.lean: finiteness of the tensor products

Estimated changes

deleted theorem AlgHom.Finite.comp
deleted theorem AlgHom.Finite.id
deleted def AlgHom.Finite
deleted theorem Ideal.FG.map
deleted def Ideal.FG
deleted theorem Ideal.fg_ker_comp
deleted theorem Module.Finite.equiv
deleted theorem Module.Finite.equiv_iff
deleted theorem Module.Finite.exists_fin'
deleted theorem Module.Finite.exists_fin
deleted theorem Module.Finite.iff_fg
deleted theorem Module.Finite.trans
deleted theorem Module.finite_def
deleted theorem Module.finite_iff_finite
deleted theorem Module.finite_of_finite
deleted theorem RingHom.Finite.comp
deleted theorem RingHom.Finite.id
deleted def RingHom.Finite
deleted theorem Set.Finite.submoduleSpan
deleted theorem Submodule.FG.map
deleted theorem Submodule.FG.map₂
deleted theorem Submodule.FG.mul
deleted theorem Submodule.FG.pow
deleted theorem Submodule.FG.prod
deleted theorem Submodule.FG.sup
deleted def Submodule.FG
deleted theorem Submodule.fg_biSup
deleted theorem Submodule.fg_bot
deleted theorem Submodule.fg_def
deleted theorem Submodule.fg_finset_sup
deleted theorem Submodule.fg_iSup
deleted theorem Submodule.fg_iff_compact
deleted theorem Submodule.fg_induction
deleted theorem Submodule.fg_ker_comp
deleted theorem Submodule.fg_of_fg_map
deleted theorem Submodule.fg_of_isUnit
deleted theorem Submodule.fg_pi
deleted theorem Submodule.fg_span
deleted theorem Submodule.fg_top
deleted theorem Submodule.fg_unit
added theorem AlgHom.Finite.comp
added theorem AlgHom.Finite.id
added theorem Module.Finite.equiv
added theorem Module.Finite.iff_fg
added theorem Module.Finite.trans
added theorem RingHom.Finite.comp
added theorem RingHom.Finite.id
added theorem Submodule.FG.map
added theorem Submodule.FG.sup
added theorem Submodule.fg_biSup
added theorem Submodule.fg_bot
added theorem Submodule.fg_iSup
added theorem Submodule.fg_induction
added theorem Submodule.fg_of_fg_map
added theorem Submodule.fg_pi
added theorem Submodule.fg_span
added theorem Submodule.fg_top
added theorem Submodule.FG.map₂
added def AlgHom.Finite
added def Ideal.FG
added theorem Module.finite_def
added def RingHom.Finite
added def Submodule.FG
added theorem Submodule.fg_def
added theorem Submodule.fg_ker_comp
added theorem Ideal.FG.map
added theorem Ideal.fg_ker_comp
added theorem Submodule.FG.prod
added theorem Submodule.FG.mul
added theorem Submodule.FG.pow
added theorem Submodule.fg_of_isUnit
added theorem Submodule.fg_unit