first isomorphism theorem for algebra morphisms

Stream: Is there code for X?

[Antoine Chambert-Loir]

I can't believe that there isn't a version of docs#quotientKerEquivRange for docs#AlgHom

example {R : Type u} [CommRing R]
  (S : Type v) [CommRing S] [Algebra R S]
  (T : Type w) [CommRing T] [Algebra R T]
  (f : S →ₐ[R] T) :
  (S ⧸ (RingHom.ker f.toRingHom)) ≃ₐ[R] f.range := by
  sorry

[Antoine Chambert-Loir]

Well, it's at one step from docs#Ideal.quotientKerAlgEquivOfSurjective

[Riccardo Brasca]

It indeed seems we are missing this version (we have the one using RingHom.range in that file so I would surprised if it were elsewhere).

[Antoine Chambert-Loir]

I'll do it, but this requires a few other lemmas…

[Antoine Chambert-Loir]

Relatedly, it is very annoying to have to type RingHom.ker f.toRingHom everytime one needs to consider the kernel of a morphism of algebras… is there a better way? Should one add AlgHom.ker, etc.

[Riccardo Brasca]

What do you mean? This works

import Mathlib

variable {R A B : Type*} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B]
variable (f : A →ₐ[R] B)

#check RingHom.ker f

[Ruben Van de Velde]

You can write RingHom.ker f, no?

[Riccardo Brasca]

I agree that writing f.ker would be nicer thought

[Antoine Chambert-Loir]

maybe — but I expect to be able to write f.ker.

[Ruben Van de Velde]

Yeah, this used to be possible in lean 3, but lean 4 is stricter on dot notation. Not sure if there's a chance to change that

[Antoine Chambert-Loir]

There are also inconsistencies in notation : compare docs#Ideal.quotientKerAlgEquivOfSurjective and docs#RingHom.quotientKerEquivOfSurjective
I believe the former should be in the AlgHom namespace and not in Ideal.AlgHom…

[Antoine Chambert-Loir]

Ruben Van de Velde said:

Yeah, this used to be possible in lean 3, but lean 4 is stricter on dot notation. Not sure if there's a chance to change that

It suffices to add a definition of AlgHom.ker

[Ruben Van de Velde]

Nothing to see at docs#Ideal.AlgHom.quotientKerEquivRange

[Antoine Chambert-Loir]

(edited)

[Antoine Chambert-Loir]

(the missing function is precisely the one that is missing…)

[Riccardo Brasca]

I am not sure how to activate dot notation, currently we cannot write f.ker even if f is a RingHom.

[Riccardo Brasca]

Ah, this is just because RingHom.ker doesn't take a ring hom as argument (but a term of type RIngHomClass)

[Eric Rodriguez]

We do still have an issue asking for more extensible dot notation, right? I guess in theory this could be done via aliases right now but that seems pretty terrible

[Eric Rodriguez]

It'd be nice to be able to register specifically that RingHoms and AlgHoms can use RingHom dot notation, and if the name matches just try put it in even if it's not quite right' - on the other hand this is a bit at odds with other details of the implementation of dot notation