ring_hom_class woes

Stream: maths

[Kevin Buzzard]

I'm not very good at ring_hom_class yet. Do people have opinions about which of the functions below (ring_equiv.comp_symm, ring_equiv.symm_comp, ring_equiv.of_hom_inv'', ring_equiv.of_hom_inv'''), are worth PR'ing? The "old-fashioned way" of_hom_inv''' seems to work more nicely for me when making the final construction. Is this because I don't know some tricks? This came up in @Michail Karatarakis 's work on decomposition and inertia groups. (When #16926 is merged map_id and map_comp will need removing).

import ring_theory.ideal.local_ring

namespace ring_equiv

variables {R S : Type*}
  [non_assoc_semiring R] [non_assoc_semiring S]

-- I couldn't find these -- do we want them? And why doesn't the coercion kick in automatically?
@[simp] lemma comp_symm (e : R ≃+* S) : (e : R →+* S).comp (e.symm : S →+* R) = ring_hom.id S :=
ring_hom.ext $ e.apply_symm_apply

@[simp] lemma symm_comp (e : R ≃+* S) : (e.symm : S →+* R).comp (e : R →+* S) = ring_hom.id R :=
ring_hom.ext $ e.symm_apply_apply

#check ring_equiv.of_hom_inv -- This exists and uses ring_hom_class but I struggle to use it below

-- Here's the old-fashioned way without ring_hom_class
def of_hom_inv''  (φ : R →+* S) (ψ : S →+* R) (h1 : ∀ r, ψ (φ r) = r)
  (h2 : ∀ s, φ (ψ s) = s) : R ≃+* S :=
⟨φ, ψ, h1, h2, φ.map_mul, φ.map_add⟩

-- a variant of the old-fashioned way
def of_hom_inv''' (φ : R →+* S) (ψ : S →+* R) (h1 : ψ.comp φ = ring_hom.id R)
  (h2 : φ.comp ψ = ring_hom.id S) : R ≃+* S :=
ring_equiv.of_hom_inv'' φ ψ (ring_hom.ext_iff.1 h1) (ring_hom.ext_iff.1 h2)

end ring_equiv

namespace local_ring.residue_field

open ring_equiv

variables {R S T: Type*} [comm_ring R] [local_ring R] [comm_ring S] [local_ring S]
                         [comm_ring T] [local_ring T]

-- next two lemmas are #16916
lemma map_id : map (ring_hom.id R) = ring_hom.id (local_ring.residue_field R) :=
 ideal.quotient.ring_hom_ext $ ring_hom.ext $ λx, rfl

lemma map_comp (f : T →+* R) (g : R →+* S)
  [is_local_ring_hom f] [is_local_ring_hom g] :
map (g.comp f) = (map g).comp (map f) :=
ideal.quotient.ring_hom_ext $ ring_hom.ext $ λx, rfl

-- this is supposed to be the follow-up PR
noncomputable theory

-- The old-fashioned way works really nicely
def map_equiv (f : R ≃+* S):
 (local_ring.residue_field R) ≃+* (local_ring.residue_field S) :=
ring_equiv.of_hom_inv''' (map f) (map f.symm) (by simp [← map_comp, ← map_id])
  (by simp [← map_comp, ← map_id])

-- The question: are we supposed to be proving this using `ring_equiv.of_hom_inv` now?

def map_equiv' (f : R ≃+* S):
 (local_ring.residue_field R) ≃+* (local_ring.residue_field S) :=
-- This approach is already messier because I have to supply the coercion myself
ring_equiv.of_hom_inv (map (f : R →+* S)) (map (f.symm : S →+* R))
begin
  -- goal now contains two coercions from
  -- `local_ring.residue_field S →+* local_ring.residue_field R` to itself?
  change (map ↑(f.symm)).comp (map ↑f) = ring_hom.id (local_ring.residue_field R),
  -- don't know how to get rid of them any other way
  simp [← map_comp, ← map_id],
end
begin
  change (map ↑f).comp (map ↑(f.symm)) = ring_hom.id (local_ring.residue_field S),
  simp [← map_comp, ← map_id],
end

end local_ring.residue_field

[Kevin Buzzard]

I asked Yael about this on the Discord and they suggested not using of_hom_inv at all.

[Jireh Loreaux]

You know what, I think this is my fault. :laughing: Sorry about that. I agree with Yaël, this just shouldn't exist as defined. But I remember why it does. The issue is that the hypotheses are phrased in terms of the compositions of the coercions, when they should be phrased in terms of bare functions. I believe that I tried to do that, but it broke things later on (involving quotient rings or something if I remember correctly) and it didn't seem like there was a pretty fix, but I could have been wrong there.

#13626 was the offending PR. You are welcome to change it back (to actual ring_homs) if you want, but if you are going to do that, please make a version for non_unital_ring_hom_class for which the composition hypotheses are on bare functions.

[Jireh Loreaux]

@Kevin Buzzard If any of what i just said isn't clear, I can clarify if need be.

[Kevin Buzzard]

In the end we just used the usual constructor :-)