Zulip Chat Archive

Stream: general

Topic: Splitting `localization.lean` and `dedekind_domain.lean


Anne Baanen (Feb 21 2022 at 12:42):

Some files in ring_theory, especially localization.lean and dedekind_domain.lean are a couple thousand lines long and have a huge set of transitive dependencies. I'd like to add a couple of lemmas to those files, but it takes ages to compile currently. Anyone opposed to carving these files up into smaller pieces (with hopefully smaller imports)?

Anne Baanen (Feb 21 2022 at 12:43):

I'm thinking:

  • dedekind_domain/basic.lean: definition of is_dedekind_domain, basic lemmas
  • dedekind_domain/ideal.lean: show that is_dedekind_domain iff all fractional ideals are invertible; unique factorization of ideals
  • dedekind_domain/dvr.lean: currently just is_dedekind_domain_dvr, would be the place to add that equivalence
  • dedekind_domain/integral_closure.lean: show that the integral closure in a finite separable extension is a Dedekind domain

  • localization/basic.lean: definition of is_localization, is_localization.away; is_localization.at_prime, is_fraction_ring; comm_ring and field instances; lift; mk; alg_equiv (the .away, .at_prime and fraction_ring parts might deserve their own files)

  • localization/integer.lean: is_integer; exist_integer_multiples
  • localization/num_denom.lean: common_denom; num; denom
  • localization/submodule.lean: coe_submodule
  • localization/ideal.lean: is_localization.map_ideal, some of the ideal.quotient_map results

Eric Rodriguez (Feb 21 2022 at 12:46):

I was going to add localization.cardinality soon (tiny file, but still), so this is timely and seems like a good idea!

Anne Baanen (Feb 22 2022 at 10:20):

Thanks to @Alex J. Best and @Johan Commelin's import tool, the import graph has been halved from 832 transitive imports to 409! #12206

Yaël Dillies (Feb 22 2022 at 10:27):

Wow, this has to be one of the biggest PR ever!


Last updated: Dec 20 2023 at 11:08 UTC