End_isUnit_iff

Stream: Is there code for X?

[Xavier Xarles]

I am sure this is already in Mathlib4

import Mathlib.GroupTheory.GroupAction.Defs
import Mathlib.Algebra.Group.Units

theorem End_isUnit_iff {M:Type*} (f : Function.End M) :
    IsUnit f ↔ Function.Bijective f := by  sorry

[Adam Topaz]

I think a more idiomatic spelling would be something like the following:

def foo (M:Type*) :
    (Function.End M)ˣ ≃ (M ≃ M) :=
  sorry

[Adam Topaz]

But I can't seem to find that one either

[Eric Wieser]

I think we probably want both spellings

[Eric Wieser]

Adam's spelling we already have for Module.End and for affine maps, and possibly more

[Eric Wieser]

I think the names are a complete mess though

[Eric Wieser]

And I don't think we have the IsUnit version for (edit: m)any morphisms

[Adam Topaz]

docs#Module.End_isUnit_iff

[Adam Topaz]

That's the only one I could find

[Xavier Xarles]

Yeah, that's what I found.

[Xavier Xarles]

My proof is pretty bad...

import Mathlib.GroupTheory.GroupAction.Defs
import Mathlib.Algebra.Group.Units


theorem End_isUnit_iff {M:Type*} (f : Function.End M) :
    IsUnit f ↔ Function.Bijective f := by
  rw [@Function.bijective_iff_has_inverse]
  simp_rw [@Function.leftInverse_iff_comp,@Function.rightInverse_iff_comp]
  constructor <;> intro h
  · let ⟨u,hu⟩ := h
    use u.inv
    rw [← hu]
    exact ⟨u.inv_val,u.val_inv⟩
  · let ⟨g,hg1,hg2⟩ := h
    use {val:=f, inv:= g, val_inv:=hg2,inv_val:=hg1}

[Junyan Xu]

Found docs#Equiv.Perm.equivUnitsEnd by Loogle

[Junyan Xu]

(deleted)

[Junyan Xu]

@loogle Function.End, Units

[loogle]

:search: Equiv.Perm.equivUnitsEnd, Equiv.Perm.val_equivUnitsEnd_apply, and 4 more

[Junyan Xu]

@loogle Function.End, IsUnit

[loogle]

:shrug: nothing found

[Antoine Chambert-Loir]

On the other hand, there is docs#CategoryTheory.isUnit_iff_isIso