Zulip Chat Archive

Stream: Is there code for X?

Topic: Subalgebras over different base fields


view this post on Zulip 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.

view this post on Zulip 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 *

view this post on Zulip 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] }

view this post on Zulip 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