subsingleton (R →ₐ[R] A)

Stream: Is there code for X?

[Kevin Buzzard]

Do we have either of these?

import tactic

variables {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]

-- I couldn't find this in mathlib

lemma alg_hom.eq_of_id (f : R →ₐ[R] A) : f = algebra.of_id R A :=
alg_hom.ext $ f.commutes

instance : subsingleton (R →ₐ[R] A) :=
subsingleton.intro $ λ f g, by { rw [alg_hom.eq_of_id f, alg_hom.eq_of_id g] }

[Eric Wieser]

Or maybe unique instead of subsingleton

[Eric Wieser]

Probably if we have this it's not an instance because adding subsingleton instances is basically forbidden at this point

[Junyan Xu]

docs#alg_hom.subsingleton not an instance for performance reasons ...

[Junyan Xu]

import algebra.algebra.subalgebra.basic
variables {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
local attribute [instance] alg_hom.subsingleton
instance x : subsingleton (R →ₐ[R] A) := by apply_instance

[Kevin Buzzard]

In our application we need eq_of_id rather than the subsingleton instance. This is for proving that the identity morphism is formally smooth.

[Andrew Yang]

Is someone working on formally smooth morphisms? I just opened #15242 and #15243.

[Andrew Yang]

I could close them though. I don't need the results for now.

[Andrew Yang]

And #15244 is also related.

[Kevin Buzzard]

There's a conference going on this week and I got chatting to @Judith Ludwig and @Jackie Lang about making these definitions and proving a basic API for them.

[Kevin Buzzard]

Oh wow what an interesting coincidence! No we're just experimenting.