Image of finite-dimensional field is finite-dimensional

Stream: new members

[Sebastian Monnet]

Let $L/K$ be a field extension and let $E/K$ be a finite dimensional subfield of $L$. I want to show that for any $K$-isomorphism $\sigma : L \to L$, the $K$-algebra $\sigma(E)$ is finite-dimensional. Here is my attempt:

import field_theory.galois

lemma im_finite_dimensional {K L : Type*} [field K] [field L] [algebra K L]
{E : intermediate_field K L} (σ : L ≃ₐ[K] L) (h_findim : finite_dimensional K E):
finite_dimensional K (E.map σ.to_alg_hom) :=
begin
  let f := σ.to_alg_hom.restrict_domain E,
  have h := linear_map.finite_dimensional_range (f : ↥E →ₗ[K] L),
  have h2 : f.range = (E.map σ.to_alg_hom).to_subalgebra,
  {
    ext,
    split,
    {
      rintro ⟨a, hax⟩,
      use a,
      refine ⟨_, hax⟩,
      simp,
    },
    {
      intro hx,
      cases hx with a hx,
      cases hx with ha hax,
      use a,
      exact ha,
      exact hax,
    },
  },
  sorry,
end

At this point I would like to do something like rw h2 at h, but this doesn't work because h2 talks about f and h talks about coe f. I'm not sure how to proceed, but I suspect it must be possible in very few lines from here. Any help would be much appreciated!

[Riccardo Brasca]

finite_dimensional is defined as module.finite,so docs#module.finite.of_surjective should do the job

[Kevin Buzzard]

It's often the case that a predicate which can be pushed along an isomorphism can also be pushed along a surjection

[Sebastian Monnet]

I'm having trouble actually getting a surjection E \to E.map \sigma. I'm sure this is really straightforward but I can't find a way to define the map

[Eric Wieser]

We have that surjection already for other subtypes, just not intermediate_field

[Eric Wieser]

Something like docs#subgroup.map_equiv, it's called something different for submonoid and submodule

[Eric Wieser]

Aha, docs#mul_equiv.subgroup_equiv_map

[Eric Wieser]

So I guess we want:

• ring_equiv.subsemiring_equiv_map
• ring_equiv.semiring_equiv_map
• alg_equiv.subalgebra_equiv_map
• alg_equiv.intermediate_field_equiv_map

[Sebastian Monnet]

@Eric Wieser so you’re saying there isn’t a quick way to do this with current mathlib?

[Eric Wieser]

The definitions above should ask only be a few lines, they're just missing

[Eric Wieser]

Just copy the approach from src#mul_equiv.submonoid_equiv_map

[Eric Wieser]

A PR adding just those would be great!

[Sebastian Monnet]

Alright, I’ll do that then. Thanks for your help!

[Sebastian Monnet]

@Eric Wieser I've done most of it, although I'm not managing to get the commutes' axiom for alg_equivs. Here's what I have so far:

lemma im_in_map {K L L' : Type*} [field K] [field L] [field L']
[algebra K L] [algebra K L'] (E : intermediate_field K L) (σ : L ≃ₐ[K] L')
(x : E) :
σ x ∈ E.map σ.to_alg_hom :=
begin
  use x,
  simp,
end

lemma inv_im_in_subfield {K L L' : Type*} [field K] [field L] [field L']
[algebra K L] [algebra K L'] (E : intermediate_field K L) (σ : L ≃ₐ[K] L')
(y : E.map σ.to_alg_hom) :
σ.symm y ∈ E :=
begin
  cases y with x hx,
  cases hx with a ha,
  cases ha with ha hax,
  simp,
  rw ← hax,
  simp,
  exact ha,
end


def intermediate_field_equiv_map {K L L' : Type*} [field K] [field L] [field L']
[algebra K L] [algebra K L'] (E : intermediate_field K L) (σ : L ≃ₐ[K] L') :
E ≃ₐ[K] E.map σ.to_alg_hom :=
{ to_fun := λ x, ⟨σ x, im_in_map E σ x⟩,
  inv_fun := λ x, ⟨σ.symm x, inv_im_in_subfield E σ x⟩,
  left_inv :=
  begin
    intro x,
    simp,
  end,
  right_inv :=
  begin
    intro x,
    simp,
  end,
  map_mul' :=
  begin
    intros x y,
    simp,
    refl,
  end,
  map_add' :=
  begin
    intros x y,
    simp,
    refl,
  end,
  commutes' :=
  begin
    intro x,
    sorry,
  end
   }

Can you see a way to close the final goal? p.s. I realise my proof is extremely long compared to the submonoid one you sent me - I don't really understand the syntax in that prove with the _s and the ..s. Also I think this situation is probably harder because of the algebra structure.

[Eric Wieser]

def foo := { commutes := sorry, ..bar} means "reuse all the other fields from bar rather than reproving them"

[Sebastian Monnet]

Does that help with proving the commutes' condition? Seems like being a K-algebra is novel to this situation and can't be reused from one of the other constructions

[Eric Wieser]

You could build the alg_hom version first

[Eric Wieser]

What's the goal state that you're stuck at?

[Eric Wieser]

(I don't have Lean accessible)

[Sebastian Monnet]

I'm stuck on

⟨⇑σ ↑(⇑(algebra_map K ↥E) x), _⟩ = ⇑(algebra_map K ↥(E.map σ.to_alg_hom)) x

[Sebastian Monnet]

Which is pretty obviously true from a maths standpoint, but seems like a type-theoretic nightmare

[Eric Wieser]

ext

[Eric Rodriguez]

from toying with this, you may need subalgebra.coe_algebra_map for intermediate_fields

[Eric Wieser]

I would suggest proving this for subalgebra first

[Kevin Buzzard]

import field_theory.galois

def ring_equiv.subsemiring_equiv_map {A B : Type*} [non_assoc_semiring A]
  [non_assoc_semiring B] (e : A ≃+* B) (R : subsemiring A) :
  R ≃+* R.map e.to_ring_hom :=
{ ..e.to_add_equiv.add_submonoid_equiv_map R.to_add_submonoid,
  ..e.to_mul_equiv.submonoid_equiv_map R.to_submonoid}

def ring_equiv.subring_equiv_map {A B : Type*} [ring A]
  [ring B] (e : A ≃+* B) (R : subring A) :
  R ≃+* R.map e.to_ring_hom :=
e.subsemiring_equiv_map R.to_subsemiring


def alg_equiv.subalgebra_equiv_map {R A B : Type*} [comm_semiring R] [semiring A]
  [semiring B] [algebra R A] [algebra R B] (e : A ≃ₐ[R] B) (S : subalgebra R A) :
  S ≃ₐ[R] (S.map e.to_alg_hom) :=
{ commutes' := λ r, begin
    -- goal is equality of elements of e(S)
    ext,
    -- now an equality of elements of B
    -- but syntactically horrible
    simp,
    -- only partly fixes it
    -- ↑(⇑(e.to_ring_equiv.subsemiring_equiv_map S.to_subsemiring) (⇑(algebra_map R ↥S) r)) =
    --   ⇑(algebra_map R B) r
    change e (algebra_map R A r) = (algebra_map R B r),
    -- the cheat way to get it into simp normal form
    simp,
  end,
  ..e.to_ring_equiv.subsemiring_equiv_map S.to_subsemiring,
}

def alg_equiv.intermediate_field_equiv_map {K L M : Type*} [field K] [field L] [field M]
  [algebra K L] [algebra K M] (e : L ≃ₐ[K] M) (E : intermediate_field K L) :
  E ≃ₐ[K] (E.map e.to_alg_hom) :=
e.subalgebra_equiv_map E.to_subalgebra

I got stuck in the same place as Sebastian -- I unstucked myself with a change but should simp be doing that?

[Andrew Yang]

The problem seems to be that the new definitions added does not have accompanying simp lemmas.
adding @[simps] to ring_equiv.subsemiring_equiv_map and ring_equiv.subring_equiv_map works.

[Yakov Pechersky]

You just need a magic @[simps]:

import field_theory.galois

@[simps] def ring_equiv.subsemiring_equiv_map {A B : Type*} [non_assoc_semiring A]
  [non_assoc_semiring B] (e : A ≃+* B) (R : subsemiring A) :
  R ≃+* R.map e.to_ring_hom :=
{ ..e.to_add_equiv.add_submonoid_equiv_map R.to_add_submonoid,
  ..e.to_mul_equiv.submonoid_equiv_map R.to_submonoid}

def ring_equiv.subring_equiv_map {A B : Type*} [ring A]
  [ring B] (e : A ≃+* B) (R : subring A) :
  R ≃+* R.map e.to_ring_hom :=
e.subsemiring_equiv_map R.to_subsemiring

def alg_equiv.subalgebra_equiv_map {R A B : Type*} [comm_semiring R] [semiring A]
  [semiring B] [algebra R A] [algebra R B] (e : A ≃ₐ[R] B) (S : subalgebra R A) :
  S ≃ₐ[R] (S.map e.to_alg_hom) :=
{ commutes' := λ r, by { ext, simp },
  ..e.to_ring_equiv.subsemiring_equiv_map S.to_subsemiring }

def alg_equiv.intermediate_field_equiv_map {K L M : Type*} [field K] [field L] [field M]
  [algebra K L] [algebra K M] (e : L ≃ₐ[K] M) (E : intermediate_field K L) :
  E ≃ₐ[K] (E.map e.to_alg_hom) :=
e.subalgebra_equiv_map E.to_subalgebra

[Eric Wieser]

(these are now in #11168)