Try to write `AlgEquiv.irreducible_map_iff`

Stream: new members

[Nick_adfor]

I was trying to formalize "No polynomial ring with more than one indeterminant is a PID. I have write a construction (Thanks for instant help from@Junyan Xu). But have xi_irr : Irreducible xi seem to be a little hard to prove. AlgEquiv.irreducible_map_iff is not a theorem in Mathlib and I don't know how to write it.

import Mathlib

open MvPolynomial Ideal

variable (R : Type*) [Field R] [DecidableEq R]
variable (σ : Type*) [Fintype σ] [DecidableEq σ] [Nonempty σ]

theorem mvPolynomial_not_pid_of_card_ge_two (h : 2 ≤ Fintype.card σ) :
    ¬ IsPrincipalIdealRing (MvPolynomial σ R) := by
  obtain ⟨i, j, hij⟩ := Fintype.exists_pair_of_one_lt_card h
  intro hPID
  let xi : MvPolynomial σ R := X i
  have xi_irr : Irreducible xi := by
    let remaining_vars : Finset σ := Finset.univ.erase i
    let e : σ ≃ Option remaining_vars := by
      letI : Fintype remaining_vars := Finset.fintypeCoeSort remaining_vars
      sorry
    let φ : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Option remaining_vars) R := renameEquiv R e
    let ψ : MvPolynomial (Option remaining_vars) R ≃ₐ[R] Polynomial (MvPolynomial remaining_vars R) := optionEquivLeft R remaining_vars
    let iso := φ.trans ψ
    have h_iso: iso xi = Polynomial.X := by
      simp [xi, renameEquiv, rename_X, optionEquivLeft, e]
      sorry
    have : Irreducible (iso xi) := by
      rw [h_iso]
      exact Polynomial.irreducible_X
    sorry--This part seem to need a `AlgEquiv.irreducible_map_iff`, but Mathlib does not have it yet.
  let I := Ideal.span ({xi} : Set (MvPolynomial σ R))
  have hmax: IsMaximal (I) :=
    PrincipalIdealRing.isMaximal_of_irreducible xi_irr
  have not_mem : X j ∉ I := by
    intro h'
    rw [mem_span_singleton, X_dvd_X] at h'
    exact hij h'
  have : I + Ideal.span {X j} = ⊤ :=
    hmax.out.sup_eq_top_iff.mpr (mt I.span_singleton_le_iff_mem.mp not_mem)--This part can only work on the latest version, but can work on Lean 4 web. What happened to the version change?
  rw [Ideal.eq_top_iff_one] at this
  obtain ⟨p, hp, q, hq, hpq⟩ := Submodule.mem_sup.mp this
  obtain ⟨p, rfl⟩ := mem_span_singleton.mp hp
  obtain ⟨q, rfl⟩ := mem_span_singleton.mp hq
  apply_fun (eval fun _ ↦ 0) at hpq
  simp [xi] at hpq

[Riccardo Brasca]

Note that we have MulEquiv.irreducible_iff, so in practice we already have a more general version of AlgEquiv.irreducible_map_iff.

[Nick_adfor]

Riccardo Brasca said:

Note that we have MulEquiv.irreducible_iff, so in practice we already have a more general version of AlgEquiv.irreducible_map_iff.

Thanks! But I find another question that AlgEquiv.toMulEquiv is not in Mathlib : (

[Aaron Liu]

Use docs#MulEquivClass.toMulEquiv

[Aaron Liu]

it's registered as a coercion

[Aaron Liu]

I'm not completely convinced that this is a good idea from a library design perspective but this is what we have

[Nick_adfor]

Aaron Liu said:

Use docs#MulEquivClass.toMulEquiv

Thanks for that. exact (MulEquivClass.toMulEquiv iso).irreducible_iff.mp this solves the last sorry : ) (Can work on v4.16.0 but not on lean 4 web)

I used to think that this kind of one-line exact can be generated by exact?. But today, it seems that exact? is not so useful : (

[Nick_adfor]

And what about:

    let e : σ ≃ Option remaining_vars := by
      letI : Fintype remaining_vars := Finset.fintypeCoeSort remaining_vars
      sorry

    have h_iso: iso xi = Polynomial.X := by
      simp [xi, renameEquiv, rename_X, optionEquivLeft, e]
      sorry

[Junyan Xu]

MulEquiv.irreducible_iff takes MulEquivClass as input so you shouldn't even need to use MulEquivClass.toMulEquiv

[Nick_adfor]

The whole code in v4.16.0 is as follows. Thanks for all.

import Mathlib.Algebra.MvPolynomial.Division
import Mathlib.Algebra.Polynomial.RingDivision
import Mathlib.RingTheory.Henselian
import Mathlib.RingTheory.Polynomial.Basic

open MvPolynomial Ideal

variable (R : Type*) [Field R]
variable (σ : Type*) [Fintype σ] [DecidableEq σ]

--These two theorems are copied from v4.22.0. They are not in v4.16.0.
theorem IsAtom.inf_eq_bot_iff [SemilatticeInf α] [OrderBot α] {a b : α} (ha : IsAtom a) :
    a ⊓ b = ⊥ ↔ ¬ a ≤ b := by
  by_cases hb : b = ⊥
  · simpa [hb] using ha.1
  · exact ⟨fun h ↦ inf_lt_left.mp (h ▸ bot_lt ha), fun h ↦ ha.2 _ (inf_lt_left.mpr h)⟩

theorem IsCoatom.sup_eq_top_iff [SemilatticeSup α] [OrderTop α] {a b : α} (ha : IsCoatom a) :
    a ⊔ b = ⊤ ↔ ¬ b ≤ a :=
  ha.dual.inf_eq_bot_iff

theorem mvPolynomial_not_pid_of_card_ge_two (h : 2 ≤ Fintype.card σ) :
    ¬ IsPrincipalIdealRing (MvPolynomial σ R) := by
  obtain ⟨i, j, hij⟩ := Fintype.exists_pair_of_one_lt_card h
  intro hPID
  let xi : MvPolynomial σ R := X i
  have xi_irr : Irreducible xi := by
    let remaining_vars : Finset σ := Finset.univ.erase i
    let e : σ ≃ Option remaining_vars := by
      letI : Fintype remaining_vars := Finset.fintypeCoeSort remaining_vars
      refine
      { toFun := fun x => if h : x = i then none else some ⟨x, Finset.mem_erase.mpr ⟨h, Finset.mem_univ _⟩⟩
        invFun := fun o => o.elim i (↑)
        left_inv := by
          intro x
          dsimp
          by_cases h : x = i
          · simp [h]
          · simp only [h, dite_false]
            rw [Option.elim_some]
        right_inv := by
          intro o
          cases o with
          | none => simp
          | some val =>
            simp
            exact (Finset.mem_erase.mp val.2).1 }
    let φ : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Option remaining_vars) R := renameEquiv R e
    let ψ : MvPolynomial (Option remaining_vars) R ≃ₐ[R] Polynomial (MvPolynomial remaining_vars R) := optionEquivLeft R remaining_vars
    let iso := φ.trans ψ
    have h_iso: iso xi = Polynomial.X := by
      rw [AlgEquiv.trans_apply, renameEquiv_apply, rename_X]
      have e_i_eq_none : e i = none := by
        simp [e]
      rw [e_i_eq_none, optionEquivLeft_X_none]
    have : Irreducible (iso xi) := by
      rw [h_iso]
      exact Polynomial.irreducible_X
    exact (MulEquivClass.toMulEquiv iso).irreducible_iff.mp this
  let I := Ideal.span ({xi} : Set (MvPolynomial σ R))
  have hmax: IsMaximal (I) :=
    PrincipalIdealRing.isMaximal_of_irreducible xi_irr
  have not_mem : X j ∉ I := by
    intro h'
    rw [mem_span_singleton, X_dvd_X] at h'
    exact hij h'
  have : I + Ideal.span {X j} = ⊤ :=
    hmax.out.sup_eq_top_iff.mpr (mt I.span_singleton_le_iff_mem.mp not_mem)--Use two theorems in v4.22.0 but not in v4.16.0.
  rw [Ideal.eq_top_iff_one] at this
  obtain ⟨p, hp, q, hq, hpq⟩ := Submodule.mem_sup.mp this
  obtain ⟨p, rfl⟩ := mem_span_singleton.mp hp
  obtain ⟨q, rfl⟩ := mem_span_singleton.mp hq
  apply_fun (eval fun _ ↦ 0) at hpq
  simp [xi] at hpq

[Nick_adfor]

Junyan Xu said:

MulEquiv.irreducible_iff takes MulEquivClass as input so you shouldn't even need to use MulEquivClass.toMulEquiv

In my code I use exact (MulEquivClass.toMulEquiv iso).irreducible_iff.mp this, it can work on v4.16.0 but not on v4.22.0. What happened to the version change : (

[Riccardo Brasca]

Just use exact (MulEquiv.irreducible_iff iso).mp this.

[Nick_adfor]

PrincipalIdealRing.isMaximal_of_irreducible also cannot use in the latest version.

[Nick_adfor]

Riccardo Brasca said:

Just use exact (MulEquiv.irreducible_iff iso).mp this.

Quite thanks : )

[Nick_adfor]

Nick_adfor said:

PrincipalIdealRing.isMaximal_of_irreducible also cannot use in the latest version.

Yet this one with a sorry can work

[Nick_adfor]

I seem to find the reason: in v 4.16.0, import Mathlib.RingTheory.Henselian seem to conclude import Mathlib.RingTheory.PrincipalIdealDomain, so if I use #min_imports, import Mathlib.RingTheory.PrincipalIdealDomain won't appear in Infoview. But in v4.22.0, import Mathlib.RingTheory.PrincipalIdealDomain is necesarry.