Integral adjoin is finite-dimensional

Stream: Is there code for X?

[Michał Staromiejski]

Do we have this result in Mathlib?

import Mathlib.Algebra.Algebra.Subalgebra.Basic
import Mathlib.LinearAlgebra.FiniteDimensional.Defs
import Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs

example {F A : Type*} [Field F] [CommRing A] [Algebra F A] {a : A} (hai : IsIntegral F a) :
    FiniteDimensional F (Algebra.adjoin F {a}) := sorry

Seems basic but I can't find it.

[Riccardo Brasca]

We surely have it in some form, let me have a look

[Michał Staromiejski]

Another question: why can't I make it an instance? This does not work:

import Mathlib.Algebra.Algebra.Subalgebra.Basic
import Mathlib.LinearAlgebra.FiniteDimensional.Defs
import Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs

instance {F A : Type*} [Field F] [CommRing A] [Algebra F A] {a : A} (hai : IsIntegral F a) :
    FiniteDimensional F (Algebra.adjoin F {a}) := sorry

example {F A : Type*} [Field F] [CommRing A] [Algebra F A] {a : A} (hai : IsIntegral F a)  : ... :=
  haveI : FiniteDimensional F (Algebra.adjoin F {a}) := inferInstance
  sorry

[Michał Staromiejski]

Riccardo Brasca said:

We surely have it in some form, let me have a look

We have FiniteDimensional.of_fintype_basis and Algebra.adjoin.powerBasisAux so the proof is easy, but could not find anything else.

[Riccardo Brasca]

import Mathlib

example {F A : Type*} [Field F] [CommRing A] [Algebra F A] {a : A} (hai : IsIntegral F a) :
    FiniteDimensional F (Algebra.adjoin F {a}) :=
  PowerBasis.finite (Algebra.adjoin.powerBasis hai)

[Riccardo Brasca]

Yes, that is what I mean, is "almost" there

[Riccardo Brasca]

Michał Staromiejski said:

Another question: why can't I make it an instance? This does not work:

import Mathlib.Algebra.Algebra.Subalgebra.Basic
import Mathlib.LinearAlgebra.FiniteDimensional.Defs
import Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs

instance {F A : Type*} [Field F] [CommRing A] [Algebra F A] {a : A} (hai : IsIntegral F a) :
    FiniteDimensional F (Algebra.adjoin F {a}) := sorry

example {F A : Type*} [Field F] [CommRing A] [Algebra F A] {a : A} (hai : IsIntegral F a)  : ... :=
  haveI : FiniteDimensional F (Algebra.adjoin F {a}) := inferInstance
  sorry

Because of the assumption hai, that is not a typeclass assumption.

[Riccardo Brasca]

If you write

import Mathlib

instance {F A : Type*} [Field F] [CommRing A] [Algebra F A] {a : A} (hai : IsIntegral F a) :
    FiniteDimensional F (Algebra.adjoin F {a}) :=
  PowerBasis.finite (Algebra.adjoin.powerBasis hai)

#lint

you see the error

/- The `impossibleInstance` linter reports:
SOME INSTANCES HAVE ARGUMENTS THAT ARE IMPOSSIBLE TO INFER
These are arguments that are not instance-implicit and do not appear in
another instance-implicit argument or the return type. -/

[Michał Staromiejski]

Thanks! Do we want this theorem in direct form? I think it might be useful?

[Riccardo Brasca]

It looks fine to me, but be sure to provide also the more general case with a finite set

[Andrew Yang]

There’s also docs#Algebra.IsIntegral.finite

[Michał Staromiejski]

This, combined with docs#Algebra.IsIntegral.adjoin would do the trick :tada:

[Riccardo Brasca]

You still have to prove that Algebra.FiniteType F (Algebra.adjoin F {a}), that I am bit surprised is not there (not difficult, but is should be automatic).

[Riccardo Brasca]

Also, note that if you use Module.Finite instead of FiniteDimensional you can state and prove a more general version, with F a CommRing.

[Michał Staromiejski]

Yup, thanks. Will try to prove general version.

[Michał Staromiejski]

Is there a reason why docs#Algebra.IsIntegral.finite is in Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic and not for example in Mathlib.RingTheory.IntegralClosure.Algebra.Basic?

[Michał Staromiejski]

It seems that actually a lot of results in Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic are results just about Algebra.IsIntegral so it seems that they should rather belong to Mathlib.RingTheory.IntegralClosure.Algebra.Basic but maybe I'm missing something?

[Michał Staromiejski]

Ok, docs#Algebra.IsIntegral.adjoin uses integralClosure so maybe it's ok. Then I'd add the results there.

[Michał Staromiejski]

So, Algebra.FiniteType F (Algebra.adjoin F {a}) is there (almost): docs#IsIntegral.fg_adjoin_singleton
and for finite set S there is docs#Subalgebra.fg_adjoin_finset.

Quite far form each other, but still there :)

[Michał Staromiejski]

PR #20970 created.

[Junyan Xu]

Did you notice that docs#fg_adjoin_of_finite and docs#IsIntegral.fg_adjoin_singleton are about finite generation of the submodule, not the subalgebra? So all you need is to use docs#Module.Finite.iff_fg.

[Michał Staromiejski]

Good point! Now they're just one-liners and I moved them to Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic. But maybe ...Algebra.Basic is a better place?