NYLL
Module

Ideal_exists_ne_zero_and_forall_isMaximal_radical_map_isPrime.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_exists_ne_zero_and_forall_isMaximal_radical_map_isPrime
9 declarations indexed from sourceView source ↗

Module documentation

Ideal exists ne zero and forall is Maximal radical map is Prime

Imports4
Imported by2

Declarations

theorem

nilradical_isPrime_of_radicial

L33 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_ne_zero_and_forall_isMaximal_radical_map_isPrime.P2mGenIrredAff.nilradical_isPrime_of_radicial
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_ne_zero_and_forall_isMaximal_radical_map_isPrime
universe u v w
namespace P2mGenIrredAff
open Ideal
Lean source · statement
theorem nilradical_isPrime_of_radicial {A D : Type*} [CommRing A] [Nontrivial A] [CommRing D]
  [IsDomain D]
    (j : D →+* A) (hj : Function.Injective j) (g : A)
    (hg : ∀ Q ∈ minimalPrimes A, g ∉ Q)
    (hrad : ∀ a : A, ∃ m M : ℕ, 0 < M ∧ (g ^ m * a) ^ M ∈ j.range) :
    (nilradical A).IsPrime
lemma

optionEquivLeft_symm_C

L89 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_ne_zero_and_forall_isMaximal_radical_map_isPrime.P2mGenIrredAff.optionEquivLeft_symm_C
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_ne_zero_and_forall_isMaximal_radical_map_isPrime
universe u v w
namespace P2mGenIrredAff
open Ideal
section OptionEquiv
variable {R S : Type*} [CommRing R] [CommRing S] {σ : Type*}
Lean source · statement
lemma optionEquivLeft_symm_C (p : MvPolynomial σ R) :
    (MvPolynomial.optionEquivLeft R σ).symm (Polynomial.C p) = MvPolynomial.rename some p
lemma

map_optionEquivLeft_symm

L93 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_ne_zero_and_forall_isMaximal_radical_map_isPrime.P2mGenIrredAff.map_optionEquivLeft_symm
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_ne_zero_and_forall_isMaximal_radical_map_isPrime
universe u v w
namespace P2mGenIrredAff
open Ideal
section OptionEquiv
variable {R S : Type*} [CommRing R] [CommRing S] {σ : Type*}
Lean source · statement
lemma map_optionEquivLeft_symm (f : R →+* S) (F : Polynomial (MvPolynomial σ R)) :
    MvPolynomial.map f ((MvPolynomial.optionEquivLeft R σ).symm F) =
      (MvPolynomial.optionEquivLeft S σ).symm (F.map (MvPolynomial.map f))
lemma

aeval_optionEquivLeft_symm

L110 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_ne_zero_and_forall_isMaximal_radical_map_isPrime.P2mGenIrredAff.aeval_optionEquivLeft_symm
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_ne_zero_and_forall_isMaximal_radical_map_isPrime
universe u v w
namespace P2mGenIrredAff
open Ideal
section OptionEquiv
variable {R S : Type*} [CommRing R] [CommRing S] {σ : Type*}
Lean source · full declaration
lemma aeval_optionEquivLeft_symm {C : Type*} [CommRing C] [Algebra R C] {d : ℕ}
    (z : Fin d → C) (w : C) (F : Polynomial (MvPolynomial (Fin d) R)) :
    MvPolynomial.aeval (fun o : Option (Fin d) => o.elim w z) ((MvPolynomial.optionEquivLeft R (Fin
      d)).symm F) =
      F.eval₂ (MvPolynomial.aeval z : MvPolynomial (Fin d) R →ₐ[R] C).toRingHom w := by
  rw [MvPolynomial.aeval_def, ← MvPolynomial.eval_map, map_optionEquivLeft_symm,
    MvPolynomial.optionEquivLeft_elim_eval, AlgEquiv.apply_symm_apply, Polynomial.map_map,
    Polynomial.eval_map]
  congr 1
  apply MvPolynomial.ringHom_ext
  · intro r
    simp
  · intro i
    simp
theorem

ringKrullDim_le_of_isIntegral

L129 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_ne_zero_and_forall_isMaximal_radical_map_isPrime.P2mGenIrredAff.ringKrullDim_le_of_isIntegral
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_ne_zero_and_forall_isMaximal_radical_map_isPrime
universe u v w
namespace P2mGenIrredAff
open Ideal
section General
Lean source · statement
theorem ringKrullDim_le_of_isIntegral {B S : Type*} [CommRing B] [CommRing S] (f : B →+* S)
    (hf : f.IsIntegral) : ringKrullDim S ≤ ringKrullDim B
theorem

radical_eq_comap_nilradical

L142 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_ne_zero_and_forall_isMaximal_radical_map_isPrime.P2mGenIrredAff.radical_eq_comap_nilradical
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_ne_zero_and_forall_isMaximal_radical_map_isPrime
universe u v w
namespace P2mGenIrredAff
open Ideal
section General
Lean source · statement
theorem radical_eq_comap_nilradical {C : Type*} [CommRing C] (I : Ideal C) :
    I.radical = (nilradical (C ⧸ I)).comap (Ideal.Quotient.mk I)
theorem

comap_mem_minimalPrimes

L152 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_ne_zero_and_forall_isMaximal_radical_map_isPrime.P2mGenIrredAff.comap_mem_minimalPrimes
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_ne_zero_and_forall_isMaximal_radical_map_isPrime
universe u v w
namespace P2mGenIrredAff
open Ideal
section General
Lean source · statement
theorem comap_mem_minimalPrimes {C : Type*} [CommRing C] (I : Ideal C) {Qb : Ideal (C ⧸ I)}
    (hQb : Qb ∈ minimalPrimes (C ⧸ I)) : Qb.comap (Ideal.Quotient.mk I) ∈ I.minimalPrimes
theorem

main

L181 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_ne_zero_and_forall_isMaximal_radical_map_isPrime.P2mGenIrredAff.main
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_ne_zero_and_forall_isMaximal_radical_map_isPrime
universe u v w
namespace P2mGenIrredAff
open Ideal
section Main
variable (k : Type u) [Field k] {R : Type v} {C : Type w} [CommRing R] [IsDomain R] [Algebra k R]
    [Algebra.FiniteType k R] [CommRing C] [IsDomain C] [Algebra k C] [Algebra R C]
    [IsScalarTower k R C] [Algebra.FiniteType R C] [FaithfulSMul R C]
Lean source · statement
theorem main
    (hgi : ∀ θ : FractionRing C,
      IsSeparable (IntermediateField.adjoin k (Set.range (algebraMap R (FractionRing C)))) θ →
      θ ∈ IntermediateField.adjoin k (Set.range (algebraMap R (FractionRing C)))) :
    ∃ r : R, r ≠ 0 ∧ ∀ n : Ideal R, n.IsMaximal → r ∉ n →
      n.map (algebraMap R C) = ⊤ ∨ (n.map (algebraMap R C)).radical.IsPrime
theorem

exists_ne_zero_and_forall_isMaximal_radical_map_isPrime

L499 ↗
Ideal.exists_ne_zero_and_forall_isMaximal_radical_map_isPrime
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_ne_zero_and_forall_isMaximal_radical_map_isPrime
universe u v w
Lean source · statement
theorem _root_.Ideal.exists_ne_zero_and_forall_isMaximal_radical_map_isPrime
    (k : Type u) [Field k] {R : Type v} {C : Type w} [CommRing R] [IsDomain R] [Algebra k R]
    [Algebra.FiniteType k R] [CommRing C] [IsDomain C] [Algebra k C] [Algebra R C]
    [IsScalarTower k R C] [Algebra.FiniteType R C] [FaithfulSMul R C]
    (hgi : ∀ θ : FractionRing C,
      IsSeparable (IntermediateField.adjoin k (Set.range (algebraMap R (FractionRing C)))) θ →
      θ ∈ IntermediateField.adjoin k (Set.range (algebraMap R (FractionRing C)))) :
    ∃ r : R, r ≠ 0 ∧ ∀ n : Ideal R, n.IsMaximal → r ∉ n →
      n.map (algebraMap R C) = ⊤ ∨ (n.map (algebraMap R C)).radical.IsPrime

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.