[Merged by Bors] - chore(*): review some lemmas about injectivity of coercions

[urkud]

API changes:

• rename linear_map.coe_fn_congr to protected linear_map.congr_arg;
• rename linear_map.lcongr_fun to protected linear_map.congr_fun;
• rename enorm.coe_fn_injective to enorm.injective_coe_fn, add
  enorm.coe_inj;
• rename equiv.coe_fn_injective to equiv.injective_coe_fn,
  reformulate in terms of function.injective;
• add equiv.coe_inj;
• add affine_map.injective_coe_fn, protected affine_map.congr_arg,
  and protected affine_map.congr_fun;
• rename linear_equiv.to_equiv_injective to
  linear_equiv.injective_to_equiv, add linear_equiv.to_equiv_inj;
• rename linear_equiv.eq_of_linear_map_eq to
  linear_equiv.injective_to_linear_map, formulate as injective coe;
• add linear_equiv.to_linear_map_inj;
• rename outer_measure.coe_fn_injective to
  outer_measure.injective_coe_fn;
• rename rel_iso.to_equiv_injective to rel_iso.injective_to_equiv;
• rename rel_iso.coe_fn_injective to rel_iso.injective_coe_fn;
• rename continuous_linear_map.coe_fn_injective to
  injective_coe_fn.

---

[jcommelin]

Should we define a congr_arg and congr_fun for arbitrary bundled_hom, and then move bundled_hom as low in the hierarchy as possible?

(Aside, this could also enable goofy notation, like:

infixr ` =. `:40 := bundled_hom.congr_fun
infixl ` .= `:40 := bundled_hom.congr_arg

example (x y z : M) (f g : M →* N) : true :=
begin
  have Hfg : f = g := sorry,
  have Hxy : x = y := sorry,
  have foo := f .= Hxy,
  have bar := Hfg =. x,
  -- from the goal state:
  --   foo: ⇑f x = ⇑f y
  --   bar: ⇑f x = ⇑g x
end

)

[urkud]

I don't think that Lean 3 is so good with substructures.

[urkud]

If has_coe_to_fun was a two-argument typeclass has_coe_to_fun (src tgt : Type*) or has_coe_to_fun (src : Type*) (tgt : src → Type*), then it would be possible to write a bundled_hom typeclass.

[jcommelin]

bundled_hom already exists. It is more restricted than has_coe_to_fun. But linear_map, monoid_hom, and all the others are instances, as part of the category setup.

[urkud]

Category theory bundled hom won't work for maps between types in different universes

[urkud]

And I don't know how to write a congr_fun/congr_arg lemma that will actually work for any bundled hom.

[jcommelin]

Hmm, good point. Stupid universes 🙃 😀

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests