subring of field is integral domain

Stream: new members

[Chengyan Hu]

Hi! I'm really sorry I got stuck somewhere again. I have:

import Mathlib
open Ideal Padic Nat
variable
{L:Type*}[Field L]
{B : Type*} [CommRing B] [Algebra B L]

And I want to prove B is an integral domain.
I don't have much Idea and what I tried is

have DomainB: IsDomain B:= isDomain (B: subalgebra B L)

And it clearly failed.

[Riccardo Brasca]

This is false, isn't it? Take $B = L[X]/X^2$ and make L a B algebra via $X \mapsto 0$.

[Riccardo Brasca]

If you want B to be a subring of L than you want B : Subring L.

[Chengyan Hu]

Yeah, I hope B works as a subring. But I checked how Algebra B L works in mathlib, and I think it automatically treat it as there is an embedding?

[Chengyan Hu]

class Algebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] extends SMul R A where
  /-- Embedding `R →+* A` given by `Algebra` structure.
  Use `algebraMap` from the root namespace instead. -/
  protected algebraMap : R →+* A
  commutes' : ∀ r x, algebraMap r * x = x * algebraMap r
  smul_def' : ∀ r x, r • x = algebraMap r * x

[Kenny Lau]

the "embedding" is our "moral" way of saying things

[Kenny Lau]

we "morally" think of algebras as embeddings, but it isn't actually required to be injective

[Aaron Liu]

Every ring is an ℤ algebra, so it clearly doesn't have to be injective

[Chengyan Hu]

Ahh I see

[Kenny Lau]

it's there because that's how mathematicians think about things and talk about things

[Chengyan Hu]

Here is the whole definition of variables Kevin wrote for me, I tried to make a simplification to let it easier to read, but clearly I made a mistake. Sorry for that.

variable
    -- let K be a number field with ring of integers A
    {A K : Type*}
    [CommRing A] [IsDedekindDomain A]
    [Field K] [NumberField K] [Algebra A K]
    [IsFractionRing A K]
    [IsIntegralClosure A ℤ K]
    -- let L be an algebraic closure of K
    {L : Type*} [Field L] [Algebra K L]
    [Algebra A L] [IsScalarTower A K L]
    [IsAlgClosure K L]
    -- and let B be the integral closure of A in L
    {B : Type*} [CommRing B] [Algebra B L]
    [Algebra A B] [IsScalarTower A B L]
    [IsIntegralClosure B A L]

[Chengyan Hu]

And I really want B to be showed as an integral domain.

[Chengyan Hu]

I believe [IsIntegralClosure B A L] made things different here?

[Kenny Lau]

Chengyan Hu said:

I believe [IsIntegralClosure B A L] made things different here?

Yes, IsIntegralClosure contains an injectivity requirement.

[Chengyan Hu]

Thanks! Any suggestion on how to prove B is an integral domain here?

[Chengyan Hu]

Really no idea

[Kenny Lau]

Chengyan Hu said:

Thanks! Any suggestion on how to prove B is an integral domain here?

f is injective map, you prove xy=0 -> f(xy)=0 -> f(x)=0 or f(y)=0 -> x=0 or y=0

[Kenny Lau]

last step uses injective

[Kenny Lau]

but there might be faster proofs using Subring.instIsDomainSubtypeMem

[Chengyan Hu]

Thanks! I'll try.

[Yakov Pechersky]

Injectivity of the algebraMap as a typeclass is FaithfulSMul.

[Yakov Pechersky]

And then you use docs#Function.Injective.isDomain. There might already be an instance of a IsDomain when FaithfulSMul to a Field.

[Chengyan Hu]

yes?

[Kevin Buzzard]

@loogle IsIntegralClosure, IsDomain

[loogle]

:search: IsIntegralClosure.isField, IsIntegralClosure.isFractionRing_of_algebraic, and 45 more

[Kevin Buzzard]

@loogle IsIntegralClosure ?B ?A ?L, |- IsDomain ?B

[loogle]

:shrug: nothing found

[Kevin Buzzard]

I don't think it's there

[Chengyan Hu]

oh ok, so I have to work a bit on this seems simple but actually not thing

[Kevin Buzzard]

Here's the plan that people are suggesting:

import Mathlib

lemma isDomain_of_faithfulSMul (B L : Type*) [CommRing B] [CommRing L] [IsDomain L]
    [Algebra B L] [FaithfulSMul B L] : IsDomain B :=
  sorry

lemma faithfulSMul_of_isIntegralClosure (A B L : Type*) [CommRing A] [CommSemiring B] [CommRing L]
    [Algebra A L] [Algebra B L] [IsIntegralClosure B A L] : FaithfulSMul B L :=
  sorry

variable
    {A : Type*}
    [CommRing A]
    {L : Type*} [Field L]
    [Algebra A L]
    {B : Type*} [CommRing B] [Algebra B L]
    [Algebra A B] [IsScalarTower A B L]
    [IsIntegralClosure B A L]

example : IsDomain B := by
  have := faithfulSMul_of_isIntegralClosure A B L
  exact isDomain_of_faithfulSMul B L

[Aaron Liu]

import Mathlib

lemma isDomain_of_faithfulSMul (B L : Type*) [CommRing B] [CommRing L] [IsDomain L]
    [Algebra B L] [FaithfulSMul B L] : IsDomain B where
  mul_left_cancel_of_ne_zero := by
    intro a b c ha hbc
    apply ‹FaithfulSMul B L›.eq_of_smul_eq_smul
    intro u
    simpa [mul_smul, smul_right_inj ha] using congr($hbc • u)
  mul_right_cancel_of_ne_zero := by
    intro a c b hc hab
    rw [mul_comm a, mul_comm b] at hab
    apply ‹FaithfulSMul B L›.eq_of_smul_eq_smul
    intro u
    simpa [mul_smul, smul_right_inj hc] using congr($hab • u)
  exists_pair_ne := by
    refine ⟨0, 1, ?_⟩
    apply_fun algebraMap B L
    simp

lemma faithfulSMul_of_isIntegralClosure (A B L : Type*) [CommRing A] [CommSemiring B] [CommRing L]
    [Algebra A L] [Algebra B L] [IsIntegralClosure B A L] : FaithfulSMul B L where
  eq_of_smul_eq_smul := by
    intro a b hab
    apply IsIntegralClosure.algebraMap_injective B A L
    simpa [Algebra.algebraMap_eq_smul_one] using hab 1

variable
    {A : Type*}
    [CommRing A]
    {L : Type*} [Field L]
    [Algebra A L]
    {B : Type*} [CommRing B] [Algebra B L]
    [Algebra A B] [IsScalarTower A B L]
    [IsIntegralClosure B A L]

example : IsDomain B := by
  have := faithfulSMul_of_isIntegralClosure A B L
  exact isDomain_of_faithfulSMul B L

[Kevin Buzzard]

lemma isDomain_of_faithfulSMul (B L : Type*) [CommRing B] [CommRing L] [IsDomain L]
    [Algebra B L] [FaithfulSMul B L] : IsDomain B :=
  Function.Injective.isDomain (algebraMap B L) <| by
  rwa [← faithfulSMul_iff_algebraMap_injective B L]

lemma faithfulSMul_of_isIntegralClosure (A B L : Type*) [CommRing A] [CommSemiring B] [CommRing L]
    [Algebra A L] [Algebra B L] [IsIntegralClosure B A L] : FaithfulSMul B L where
  eq_of_smul_eq_smul {b₁ b₂} h := by
    apply IsIntegralClosure.algebraMap_injective B A L
    simp [Algebra.algebraMap_eq_smul_one, h 1]

[Yakov Pechersky]

Right, these can't be an instance because it wouldn't be able to guess the target field etc