Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-01 21:31 e0a4dd88

View on Github →

feat(ring_theory/finiteness): improve API for finite presentation (#6382) Improve the API for finitely presented morphism. I changed the name from algebra.finitely_presented to algebra.finite_presentation that seems more coherent with the other names. Coming soon: transitivity of finite presentation.

Estimated changes

Modified src/ring_theory/finiteness.lean

added theorem alg_hom.finite_presentation.comp_surjective

added theorem alg_hom.finite_presentation.id

added theorem alg_hom.finite_presentation.of_finite_type

added theorem alg_hom.finite_presentation.of_surjective

added def alg_hom.finite_presentation

added theorem alg_hom.finite_type.of_finite_presentation

added theorem algebra.finite_presentation.equiv

added theorem algebra.finite_presentation.iff_quotient_mv_polynomial'

added theorem algebra.finite_presentation.mv_polynomial

added theorem algebra.finite_presentation.of_finite_type

added theorem algebra.finite_presentation.of_surjective

added theorem algebra.finite_presentation.quotient

added theorem algebra.finite_presentation.self

added def algebra.finite_presentation

added theorem algebra.finite_type.of_finite_presentation

deleted theorem algebra.finite_type.of_finitely_presented

deleted theorem algebra.finitely_presented.equiv

deleted theorem algebra.finitely_presented.mv_polynomial

deleted theorem algebra.finitely_presented.of_surjective

deleted theorem algebra.finitely_presented.quotient

deleted theorem algebra.finitely_presented.self

deleted def algebra.finitely_presented

added theorem ring_hom.finite_presentation.comp_surjective

added theorem ring_hom.finite_presentation.id

added theorem ring_hom.finite_presentation.of_finite_type

added theorem ring_hom.finite_presentation.of_surjective

added def ring_hom.finite_presentation

added theorem ring_hom.finite_type.of_finite_presentation