Transfering algebra structure via ring homomorphism

Stream: Is there code for X?

[Michał Staromiejski]

From time to time in my proofs I encounter a need to transfer Algebra R A structure via a ring homomorphism f : A →+* B to get compatible Algebra R B (so that I can lift f to an algebra homomorphism). It can be done quite simply:

import Mathlib.Algebra.Algebra.Defs

/-- Transfer `R`-algebra structure via ring homomorphism. -/
def Algebra.of_algebra_of_ringHom (R : Type*) {A B : Type*} [CommSemiring R] [Semiring A]
    [CommSemiring B] [Algebra R A] (f : A →+* B) : Algebra R B :=
  f.comp (algebraMap R A) |>.toAlgebra

and I could not find this kind of tool in Mathlib, so maybe we want it?

I was also thinking to make a version that can return both Algebra R B and the lifted f:

def Algebra.of_algebra_of_ringHom₂ (R : Type*) {A B : Type*} [CommSemiring R] [Semiring A]
    [CommSemiring B] [Algebra R A] (f : A →+* B) : (_ : Algebra R B) ×' (A →ₐ[R] B) :=
  letI inst := of_algebra_of_ringHom R f; ⟨inst, ⟨f, fun _r ↦ rfl⟩⟩

and it kind of works but in some cases creates unexpected results:

example (R : Type*) {A B C : Type*} [CommSemiring R] [Semiring A] [CommSemiring B] [CommSemiring C]
    [Algebra R A] (f : A →+* B × C) : ... :=
  letI ⟨algBC, f'⟩ := Algebra.of_algebra_of_ringHom₂ R f /- `Algebra R (B × C)` and lifted `f` -/
  letI algB := Algebra.of_algebra_of_ringHom R (RingHom.fst B C) /- `Algebra R B` -/
  letI algC := Algebra.of_algebra_of_ringHom R (RingHom.snd B C) /- `Algebra R C` -/
  let g := (AlgHom.fst R B C).comp f' /- error -/

Error in the last line occures because I guess for AlgHom.fst R B C the Algebra R (B × C) structure comes from the instance Prod.algebra, wheras the one for f' is algBC which is a different 'object', even if it contains same data (not definitionally equal). Is there any mechanism that allows AlgHom.fst R B C to take the structure from the local context?

[Michał Staromiejski]

Ok, I think clean solution would be to use lifts at each stage and use the lift of RingHom.fst B C instead of AlgHom.fst R B C:

example (R : Type*) {A B C : Type*} [CommSemiring R] [Semiring A] [CommSemiring B] [CommSemiring C]
    [Algebra R A] (f' : A →+* B × C) : ... :=
  letI ⟨algBC, f⟩ := Algebra.of_algebra_of_ringHom₂ R f' /- `Algebra R (B × C)` and lifted `f'` -/
  letI ⟨algB, g⟩ := Algebra.of_algebra_of_ringHom₂ R (RingHom.fst B C) /- `Algebra R B` + lift of `RingHom.fst` -/
  letI ⟨algC, h⟩ := Algebra.of_algebra_of_ringHom₂ R (RingHom.snd B C) /- `Algebra R C` + lift -/
  let k := g.comp f /- ok -/

[Michał Staromiejski]

I'd add this to Mathlib, any suggestions for a good name(s)?

[Eric Wieser]

docs#Algebra.compHom

[Eric Wieser]

Ah, this is the wrong argument for you

[Johan Commelin]

@Michał Staromiejski Maybe something like Algebra.ofCompRight?

[Johan Commelin]

And yes, adding this to mathlib sounds like a good plan

[Michał Staromiejski]

@Eric Wieser this one almost feels like a dual, I'm actually surprised that it's not defined just via docs#RingHom.toAlgebra.
@Johan Commelin You mean version with lifting, right?

[Michał Staromiejski]

One more question: according to the definition of Algebra.of_algebra_of_ringHom₂ above, the toFun of both the ring hom and its lift should be defeq:

example (R : Type*) {A B : Type*} [CommSemiring R] [Semiring A] [CommSemiring B]
    [Algebra R A] {f : A →+* B} : (of_algebra_of_ringHom₂ R f).2 = f := rfl /- ok -/

However, when I use it with pattern matching (is this the right term?), it seems not to work:

example (R : Type*) {A B : Type*} [CommSemiring R] [Semiring A] [CommSemiring B]
    [Algebra R A] (f' : A →+* B) : ... :=
  let ⟨_, f⟩ := Algebra.of_algebra_of_ringHom₂ R f' /- `Algebra R B` and lifted `f'` -/
  have : f = f' := rfl /- error -/

What is going on here?

[Kevin Buzzard]

Can you give a #mwe ? I've not been following this thread and I'm not sure what goes in the ... .

[Eric Wieser]

The issue here is that pattern matching is forgetful, like have

[Eric Wieser]

If you use .1 and .2 instead it will work

[Michał Staromiejski]

Kevin Buzzard said:

Can you give a #mwe ? I've not been following this thread and I'm not sure what goes in the ... .

My original code is quite complicated but I will try with some sorries (I do have proofs for them, just wanted to simplify):

import Mathlib.Algebra.Algebra.Defs
import Mathlib.Algebra.Algebra.Hom
import Mathlib.Algebra.Ring.Prod
import Mathlib.RingTheory.LocalRing.Basic

def of_algebra_of_ringHom (R : Type*) {A B : Type*} [CommSemiring R] [Semiring A]
    [CommSemiring B] [Algebra R A] (f : A →+* B) : Algebra R B :=
  f.comp (algebraMap R A) |>.toAlgebra

def of_algebra_of_ringHom₂ (R : Type*) {A B : Type*} [CommSemiring R] [Semiring A]
    [CommSemiring B] [Algebra R A] (f : A →+* B) : (_ : Algebra R B) ×' (A →ₐ[R] B) :=
  letI inst := of_algebra_of_ringHom R f; ⟨inst, ⟨f, fun _r ↦ rfl⟩⟩

example (R : Type*) {A₁ A₂ : Type*} [CommSemiring R] [Semiring A₁] [CommSemiring A₂]
    [Algebra R A₁] {f : A₁ →+* A₂} (hf : Function.Surjective f) :
    Function.Surjective (of_algebra_of_ringHom₂ R f).2 := hf /- works -/

/-- For a non-local ring, there exists a surjection onto product of two fields. -/
lemma nonLocalProj {R : Type u} [CommRing R] [Nontrivial R] (h : ¬ IsLocalRing R) :
    ∃ (K₁ K₂ : Type u) (_ : Field K₁) (_ : Field K₂) (f : R →+* K₁ × K₂),
      Function.Surjective f := sorry

theorem bigTheorem {F A : Type*} [Field F] [CommRing A] [Algebra F A] [Nontrivial A] : IsLocalRing A := by
  by_contra h
  let ⟨K₁, K₂, fK₁, fK₂, f', hf'⟩ := nonLocalProj h
  let ⟨_, f⟩ := of_algebra_of_ringHom₂ F f'
  /- now to proceed I need: -/
  have hf : Function.Surjective f := hf'
  /- does not work either: -/
  have : f.toRingHom = f' := rfl
  sorry

It actually does not matter what is the goal here, my question is about more general setting.

@Eric Wieser Thanks, will try, although it's not very consistent then with regular let behavior...

[Michał Staromiejski]

Found also this, I'd say it is indeed an issue.

[Junyan Xu]

Does obtain work here? (I guess not)

[Michał Staromiejski]

Actually seems to work :tada:
Ah no... Lean server has stopped :rolling_on_the_floor_laughing:

[Michał Staromiejski]

Just to confirm, in the MWE above, if I use

  let alg_f := of_algebra_of_ringHom₂ F f'
  letI := alg_f.1
  let f := alg_f.2

instead of let ⟨_, f⟩ := of_algebra_of_ringHom₂ F f' then everything is fine.
But it's rather a workaround...

[Edward van de Meent]

i suspect the earlier approach might need of_algebra_of_ringHom₂ to be reducible to work, then?

[Michał Staromiejski]

@Edward van de Meent I'm quite a beginner here so not sure what that would mean?

[Jz Pan]

Michał Staromiejski said:

My original code is quite complicated but I will try with some sorries (I do have proofs for them, just wanted to simplify):

If you don't need to make your auxiliary defs public, I think maybe algebraize tactics is more suitable.

[Michał Staromiejski]

@Jz Pan Thanks for pointing it out. I had a look but not sure how would I use it in my MWE?

[Jz Pan]

I'm not familiar with it either. From the documents it seems that it can only generate Algebra and IsScalarTower automatically. Maybe let's ask the developer.