Isomorphism of algebras obtained by adjoining elements

Stream: Is there code for X?

[Dion Leijnse]

Suppose I have a commutative ring R and two R-algebras S and T, together with an R-isomorphism f : S ≃ₐ[R] T. I also have a set X : Set S. We can form the R-algebra Algebra.adjoin R X, which is the subalgebra of S formed by adjoining the set X. The map f induces an isomorphism Algebra.adjoin R X ≃ₐ[R] Algebra.adjoin R (f '' X). Is this defined somewhere in Mathlib? I could not find it so far. Here is the mwe:

import Mathlib

def adjoin_equiv (R S T : Type) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T]
    (f : S ≃ₐ[R] T) (X : Set S) : Algebra.adjoin R X ≃ₐ[R] Algebra.adjoin R (f '' X) := sorry

[Kenny Lau]

@Dion Leijnse docs#AlgHom.map_adjoin , Subalgebra.equivOfEq

[Aaron Liu]

docs#AlgEquiv.subalgebraMap, docs#AlgHom.map_adjoin, docs#Subalgebra.equivOfEq

[Dion Leijnse]

Thanks!

[Dion Leijnse]

Thanks for the help, I got it to work:

import Mathlib

def adjoin_equiv (R S T : Type) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T]
    (f : S ≃ₐ[R] T) (X : Set S) : Algebra.adjoin R X ≃ₐ[R] Algebra.adjoin R (f '' X) :=
  (AlgHom.map_adjoin f.toAlgHom X) ▸ (AlgEquiv.subalgebraMap f (Algebra.adjoin R X))

[Kenny Lau]

@Dion Leijnse please don't cast in definitions, there's a reason we both included equivOfEq

[Kevin Buzzard]

The OP might not have a clue what you're talking about.

The issue with this definition is that the ▸ is probably making a horrible term which you might find it very difficult to prove anything about.

[Dion Leijnse]

Thanks for the clarification! So the idea is to cast the equality to an equivalence, and then take the composition of the two? Something like this?

import Mathlib

def adjoin_equiv (R S T : Type) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T]
    (f : S ≃ₐ[R] T) (X : Set S) : Algebra.adjoin R X ≃ₐ[R] Algebra.adjoin R (f '' X) :=
  (AlgEquiv.subalgebraMap f (Algebra.adjoin R X)).trans
    (Subalgebra.equivOfEq _ _ (AlgHom.map_adjoin f.toAlgHom X))

[Kenny Lau]

@Dion Leijnse bingo!