therefore
Sign up
Open navigation

Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 8 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

8 results

Clear filters
Project-declaredLean 4.31.0

Mem associated Primes ker mk Linear Map of mem associated Primes of inter nonempty

HarderNarasimhan.CommutativeAlgebra.mem_associatedPrimes_ker_mkLinearMap_of_mem_associatedPrimes_of_inter_nonempty

Plain-language statement

If p is an associated prime of M and p meets the multiplicative set S, then p is an associated prime of the kernel of the localization map mkLinearMap S M : M →ₗ[R] LocalizedModule S M. This is the “meets S” direction used to identify associated primes of ker (mkLinearMap S M) with the associated primes of M that are not disjoint from...

algebraic geometryvector bundlescategory theory

Source project: Harder-Narasimhan

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Mem associated Primes of mem associated Primes quot ker mk Linear Map of disjoint

HarderNarasimhan.CommutativeAlgebra.mem_associatedPrimes_of_mem_associatedPrimes_quot_ker_mkLinearMap_of_disjoint

Project documentation

If p is an associated prime of the quotient M ⧸ ker(mkLinearMap S M) and p is disjoint from the multiplicative set S, then p is already an associated prime of M. This lemma is used to identify the “disjoint part” of the associated primes of M with the associated primes of the localization quotient.

algebraic geometryvector bundlescategory theory

Source project: Harder-Narasimhan

Person-level attribution pending.

View proof record