Where should these lemmas go?

Stream: maths

[Justus Springer]

I would like to add the fact that CommRing isomorphisms are local ring homs (see below). However, I can't decide where this should belong, as it relies both on categories and on the predicate is_local_ring_hom, which is defined in ring_theory/ideal/basic.lean. The two options I can see are:

1. ring_theory/ideal/basic.lean. But this feels a little out of place, as there are no other mentions of category theory in that file, so it would introduce a new cross-directory dependency.
2. algebra/category/CommRing/basic.lean. Here it would sort of fit in between some other facts about CommRing isomorphisms. But here too, it would introduce a cross-directory dependency to import ring_theory/ideal/basic.lean.

Any opinions? Are dependencies between different directories even something worth avoiding?

I needed this previously in Spec.lean, there I just did it manually without the abstract lemma. Now I need it again, which is why I want to add this.

import ring_theory.ideal.basic
import algebra.category.CommRing.basic

open category_theory

lemma is_local_ring_hom_of_iso {R S : CommRing} (f : R ≅ S) : is_local_ring_hom f.hom :=
{ map_nonunit := λ a ha,
begin
  convert f.inv.is_unit_map ha,
  rw coe_hom_inv_id,
end }

@[priority 100]
instance is_local_ring_hom_of_is_iso {R S : CommRing} (f : R ⟶ S) [is_iso f] :
  is_local_ring_hom f :=
is_local_ring_hom_of_iso (as_iso f)

[Yakov Pechersky]

Why not add a new file?

[Yaël Dillies]

But in which folder?

[Adam Topaz]

@Justus Springer I think this should be split up as follows.
First, we should have a variant of your is_local_ring_hom_of_iso using docs#ring_equiv as opposed to an isomoprhism in CommRing.
Second, construct a way to go from a ring_equiv to an isomorphism in CommRing (and vice versa), and lastly combine the two to obtain what you have above.

The ring_equiv version of is_local_ring_hom_of_iso should go nearby where is_local_ring_hom is defined, and the constructions relating a ring_equiv and isomorphisms in CommRing should go in the algebra/category/CommRing folder.

[Adam Topaz]

Looks like we already have docs#ring_equiv_iso_CommRing_iso and docs#category_theory.iso.CommRing_iso_to_ring_equiv

[Adam Topaz]

Arguably all the stuff near the bottom of ring_theory/ideal/basic.lean starting with src#local_ring should be in a separate file called ring_theory/local_ring.lean or something...

[Eric Wieser]

docs#is_local_ring_hom since I don't see the link upthread

[Justus Springer]

@Adam Topaz Thanks, I will try it as you describe and split the file.

[Justus Springer]

PR'd: #8849 #8850

[Kevin Buzzard]

I love the definition of local ring hom -- it reflects units

[Adam Topaz]

I'm a little surprised we didn't define is_local_ring_hom on the monoid level :wink:

[Justus Springer]

Kevin Buzzard said:

I love the definition of local ring hom -- it reflects units

Same. Only the name of the field is a little confusing: map_nonunit