Finding algebra equivalence

Stream: new members

[Francesco Minnocci]

Hi!

How would one go about proving that there is an AlgEquiv between a 1-dimensional Division Algebra A over a field F and the field itself?

I managed to prove that there is a LinearEquiv using nonempty_linearEquiv_of_finrank_eq, but what I really need is a RingEquiv which commutes with scalar multiplication.

Is there something like that in Mathlib, or do I have to build the map manually?

[Riccardo Brasca]

The map is docs#algebraMap, you can prove that it is bijective

[Riccardo Brasca]

Sorry, it's better to use docs#Algebra.ofId

[Riccardo Brasca]

Something like this

import Mathlib

open FiniteDimensional Function

variable {K A : Type*} [Field K] [Ring A] [Algebra K A] (h : finrank K A = 1)

lemma foo : Bijective (Algebra.ofId K A) := by
  have : Nontrivial A := FiniteDimensional.nontrivial_of_finrank_eq_succ h
  have : FiniteDimensional K A := finiteDimensional_of_finrank_eq_succ h
  constructor
  · exact NoZeroSMulDivisors.algebraMap_injective K A
  · show Function.Surjective (Algebra.ofId K A).toLinearMap
    rw [←LinearMap.injective_iff_surjective_of_finrank_eq_finrank (by simp [h])]
    exact NoZeroSMulDivisors.algebraMap_injective K A

noncomputable
def bar : K ≃ₐ[K] A := AlgEquiv.ofBijective (Algebra.ofId K A) (foo h)

[Riccardo Brasca]

Golfed

import Mathlib

open FiniteDimensional Algebra Subalgebra

variable {K A : Type*} [Field K] [Ring A] [Algebra K A] (h : finrank K A = 1)

noncomputable
def bar : K ≃ₐ[K] A :=
  have : Nontrivial A := FiniteDimensional.nontrivial_of_finrank_eq_succ h
  AlgEquiv.ofBijective (ofId K A) (bijective_algebraMap_iff.2 (bot_eq_top_of_finrank_eq_one h).symm)

[Francesco Minnocci]

Thanks a lot!

[Riccardo Brasca]

To find the second version I used loogle, with algebraMap, Function.Bijective

[Francesco Minnocci]

I had actually already tried using bot_eq_top_of_finrank_eq_one but had gotten stuck with it, the algebraMap business was what I missed, although mathematically is the first thing I should've looked for...

[Francesco Minnocci]

If I have an hypothesis like

∃ n, Module.rank ℝ A = ↑n

how can I close the goal

Module.rank ℝ A = ↑?n

It should be easy, but I cannot do it.

[Andrew Yang]

Is there an mwe?
I'm guessing obtain ⟨n, hn⟩ := h; exact hn would work, but it is strange that there is a metavariable ?n in the goal.

[Francesco Minnocci]

that's because I applied FiniteDimensional.finiteDimensional_of_rank_eq_nat

[Francesco Minnocci]

Thanks for the tip, obtain worked.

[Francesco Minnocci]

Why is this not closed by linarith or ring?

n: ℕ
hn: Module.rank ℝ A = ↑n
this: finrank ℝ A = n
h₁: n ≠ 0
gt₂: n < 2
⊢ n = 1

[Eric Wieser]

ring isn't intended for simultaneous equations, and maybe linarith doesn't know how to use that Nat is locally finite?

[Riccardo Brasca]

Here the goal is very easy, but for this kind of stuff you can use the fin_cases tactic. First of all you prove h : n ∈ Finset.range 2, and then you can do fin_cases h.

[Riccardo Brasca]

(deleted)

[Francesco Minnocci]

Riccardo Brasca said:

Here the goal is very easy, but for this kind of stuff you can use the fin_cases tactic. First of all you prove h : n ∈ Finset.range 2, and then you can do fin_cases h.

That works, but I'm surprised that it's not closed by any of the "automatic" tactics I know.

[Ruben Van de Velde]

I think the issue is that linarith doesn't work with naturals. Maybe omega would, but I don't think mathlib was updated to a version of std that has it yet