Commit 2024-11-25 08:40 4eab2d47

View on Github →

feat: the free locus of a (finitely presented) module (#18691)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/FinitePresentation.lean

added theorem FinitePresentation.of_isBaseChange

Created Mathlib/Algebra/Module/FreeLocus.lean

added theorem Module.basicOpen_subset_freeLocus_iff

added theorem Module.comap_freeLocus_le

added def Module.freeLocus

added theorem Module.freeLocus_congr

added theorem Module.freeLocus_eq_univ

added theorem Module.freeLocus_eq_univ_iff

added theorem Module.freeLocus_localization

added theorem Module.isLocallyConstant_rankAtStalk

added theorem Module.isLocallyConstant_rankAtStalk_freeLocus

added theorem Module.isOpen_freeLocus

added theorem Module.mem_freeLocus

added theorem Module.mem_freeLocus_iff_tensor

added theorem Module.mem_freeLocus_of_isLocalization

added def Module.rankAtStalk

Modified Mathlib/Algebra/Module/LocalizedModule/Basic.lean

added theorem IsLocalizedModule.of_exists_mul_mem

deleted theorem IsLocalizedModule.of_linearEquiv

added theorem IsLocalizedModule.of_restrictScalars

Modified Mathlib/LinearAlgebra/FreeModule/Basic.lean

added theorem Module.Free.iff_of_ringEquiv

added theorem Module.Free.of_ringEquiv

Modified Mathlib/RingTheory/Finiteness/Basic.lean

added theorem Submodule.FG.of_restrictScalars

Modified Mathlib/RingTheory/LocalProperties/Projective.lean

added theorem Module.finrank_of_isLocalizedModule_of_free

added theorem Module.free_of_isLocalizedModule

added theorem Module.lift_rank_of_isLocalizedModule_of_free