## Stream: Is there code for X?

### Topic: Subalgebras over different base fields

#### Patrick Lutz (Sep 10 2020 at 21:55):

Say that I have some subalgebras of an algebra which are over different base fields and I know some equalities between them which I want to use for a series of rewrites. Is there a really easy way to do this? Lean often seems to get confused because the types are different (even though the equalities are all really equalities on the underlying subsets of the algebra). As a mwe:

import ring_theory.algebra

variables (F E L : Type*) [field F] [field E] [field L] [algebra F E] [algebra L E]
variables (A B : subalgebra F E) (C : subalgebra L E)

example (h₁ : C = ⊤) (h₂ : A = B) (h₃ : (A : set E) = C) : ⊤ = B :=
begin
ext,
apply iff_of_true algebra.mem_top,
change x ∈ (B : set E),
rw [← h₂, h₃, h₁],
exact algebra.mem_top,
end


I feel like I should be able to prove the example above in a single line, but I don't see how to do so.

#### Kevin Buzzard (Sep 10 2020 at 22:11):

import field_theory.tower

variables (F E L : Type*) [field F] [field E] [field L] [algebra F E] [algebra L E]
variables (A B : subalgebra F E) (C : subalgebra L E)

example (h₁ : C = ⊤) (h₂ : A = B) (h₃ : (A : set E) = C) : ⊤ = B :=
by simp [subalgebra.ext_iff, set.ext_iff, algebra.mem_top, *] at *


#### Kyle Miller (Sep 10 2020 at 22:25):

A very slightly different one:

import field_theory.tower

variables (F E L : Type*) [field F] [field E] [field L] [algebra F E] [algebra L E]
variables (A B : subalgebra F E) (C : subalgebra L E)

example (h₁ : C = ⊤) (h₂ : A = B) (h₃ : (A : set E) = C) : B = ⊤ :=
by { ext, rw [←h₂, ←subalgebra.mem_coe, h₃, h₁], simp [algebra.mem_top] }


#### Patrick Lutz (Sep 10 2020 at 22:49):

Okay, nice. I had tried simp before, but not with the right lemmas I guess.

Last updated: May 17 2021 at 16:26 UTC