Composition of algebras

Stream: Is there code for X?

[Calvin Lee]

I recently had to write

instance : algebra A C := ring_hom.to_algebra $ ring_hom.comp (algebra_map B C) (algebra_map A B)

in order to "compose" two algebras algebra A B and algebra B C

this really wasn't that much work, but I'm wondering if there's a cleaner way to do it
thanks!
relevant code is here https://github.com/jjgarzella/adjunction_formula/blob/k%C3%A4hler/src/kaehler.lean#L29

[Andrew Yang]

The mathlib-correct way to set it up is [algebra A B] [algebra B C] [algebra A C] [is_scalar_tower A B C].

[Andrew Yang]

So the correct way to set up the whole file should be

variables {A B Aₛ Bₛ : Type*} [comm_ring A] [comm_ring B] [comm_ring Aₛ] [comm_ring Bₛ]
variables [algebra A B] [algebra A Aₛ] [algebra A Bₛ] [algebra Aₛ Bₛ] [algebra B Bₛ]
variables [is_scalar_tower A B Bₛ] [is_scalar_tower A Aₛ Bₛ]
variables {S : submonoid B} [is_localization S Bₛ]
variables [is_localization (algebra.algebra_map_submonoid A S) Aₛ]

[Andrew Yang]

By the way, I'm not sure if the statement stated is correct. I think it should be $\Omega_{B_T/A_T}$ with $T \subseteq A$ instead of $\Omega_{B_S/A_{f^{-1}(S)}}$ with $S \subseteq B$.

[Andrew Yang]

And I think the correct way to get that goal is to use #17198 and show that localizations are base changes.