NYLL
Module

IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq
13 declarations indexed from sourceView source ↗

Module documentation

Is Local Ring exists finite etale faithfully Flat is Local Ring sub mem maximal Ideal imp

eq

Imports7
  • Mathlib.FieldTheory.Finite.GaloisField
  • Mathlib.RingTheory.Etale.StandardEtale
  • Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
  • Mathlib.RingTheory.Ideal.GoingUp
  • Mathlib.Tactic.Choose
  • Mathlib.Tactic.LinearCombination
  • Mathlib.Tactic.Ring.RingNF
Imported by3

Declarations

def

m0

L46 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq.IsLocalRing.ResidueExtImpl.m0
Documentation

The extension of the maximal ideal to the algebra obtained by adjoining the polynomial root.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq
universe u
open _root_.Polynomial
open _root_.IsLocalRing
namespace IsLocalRing
open _root_.IsLocalRing
namespace ResidueExtImpl
open _root_.IsLocalRing
section AdjoinRoot
variable {R : Type u} [CommRing R] [IsLocalRing R] (P : R[X])
Lean source · statement
def m0 : Ideal (AdjoinRoot P)
def

quotEquiv

L50 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq.IsLocalRing.ResidueExtImpl.quotEquiv
Documentation

The quotient equivalence identifying reduction of the root algebra with the reduced polynomial root algebra.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq
universe u
open _root_.Polynomial
open _root_.IsLocalRing
namespace IsLocalRing
open _root_.IsLocalRing
namespace ResidueExtImpl
open _root_.IsLocalRing
section AdjoinRoot
variable {R : Type u} [CommRing R] [IsLocalRing R] (P : R[X])
Lean source · statement
def quotEquiv :
    AdjoinRoot P ⧸ m0 P ≃+* AdjoinRoot (P.map (residue R))
theorem

quotEquiv_mk

L54 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq.IsLocalRing.ResidueExtImpl.quotEquiv_mk
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq
universe u
open _root_.Polynomial
open _root_.IsLocalRing
namespace IsLocalRing
open _root_.IsLocalRing
namespace ResidueExtImpl
open _root_.IsLocalRing
section AdjoinRoot
variable {R : Type u} [CommRing R] [IsLocalRing R] (P : R[X])
Lean source · statement
theorem quotEquiv_mk (g : R[X]) :
    quotEquiv P (Ideal.Quotient.mk (m0 P) (AdjoinRoot.mk P g)) =
      AdjoinRoot.mk (P.map (residue R)) (g.map (residue R))
theorem

m0_isMaximal

L61 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq.IsLocalRing.ResidueExtImpl.m0_isMaximal
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq
universe u
open _root_.Polynomial
open _root_.IsLocalRing
namespace IsLocalRing
open _root_.IsLocalRing
namespace ResidueExtImpl
open _root_.IsLocalRing
section AdjoinRoot
variable {R : Type u} [CommRing R] [IsLocalRing R] (P : R[X])
variable {P}
Lean source · statement
theorem m0_isMaximal (hirr : Irreducible (P.map (residue R))) : (m0 P).IsMaximal
theorem

nontrivial

L67 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq.IsLocalRing.ResidueExtImpl.nontrivial
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq
universe u
open _root_.Polynomial
open _root_.IsLocalRing
namespace IsLocalRing
open _root_.IsLocalRing
namespace ResidueExtImpl
open _root_.IsLocalRing
section AdjoinRoot
variable {R : Type u} [CommRing R] [IsLocalRing R] (P : R[X])
variable {P}
Lean source · statement
theorem nontrivial (hirr : Irreducible (P.map (residue R))) :
    Nontrivial (AdjoinRoot P)
theorem

isLocalRing

L72 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq.IsLocalRing.ResidueExtImpl.isLocalRing
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq
universe u
open _root_.Polynomial
open _root_.IsLocalRing
namespace IsLocalRing
open _root_.IsLocalRing
namespace ResidueExtImpl
open _root_.IsLocalRing
section AdjoinRoot
variable {R : Type u} [CommRing R] [IsLocalRing R] (P : R[X])
variable {P}
Lean source · statement
theorem isLocalRing (hP : P.Monic) (hirr : Irreducible (P.map (residue R))) :
    IsLocalRing (AdjoinRoot P)
theorem

maximalIdeal_eq

L85 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq.IsLocalRing.ResidueExtImpl.maximalIdeal_eq
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq
universe u
open _root_.Polynomial
open _root_.IsLocalRing
namespace IsLocalRing
open _root_.IsLocalRing
namespace ResidueExtImpl
open _root_.IsLocalRing
section AdjoinRoot
variable {R : Type u} [CommRing R] [IsLocalRing R] (P : R[X])
variable {P}
Lean source · full declaration
theorem maximalIdeal_eq (hP : P.Monic) (hirr : Irreducible (P.map (residue R))) :
    letI := isLocalRing hP hirr
    maximalIdeal (AdjoinRoot P) = m0 P :=
  letI := isLocalRing hP hirr
  (IsLocalRing.eq_maximalIdeal (m0_isMaximal hirr)).symm
theorem

isLocalHom

L91 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq.IsLocalRing.ResidueExtImpl.isLocalHom
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq
universe u
open _root_.Polynomial
open _root_.IsLocalRing
namespace IsLocalRing
open _root_.IsLocalRing
namespace ResidueExtImpl
open _root_.IsLocalRing
section AdjoinRoot
variable {R : Type u} [CommRing R] [IsLocalRing R] (P : R[X])
variable {P}
Lean source · statement
theorem isLocalHom (hP : P.Monic) (hirr : Irreducible (P.map (residue R))) :
    IsLocalHom (algebraMap R (AdjoinRoot P))
theorem

etale

L101 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq.IsLocalRing.ResidueExtImpl.etale
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq
universe u
open _root_.Polynomial
open _root_.IsLocalRing
namespace IsLocalRing
open _root_.IsLocalRing
namespace ResidueExtImpl
open _root_.IsLocalRing
section AdjoinRoot
variable {R : Type u} [CommRing R] [IsLocalRing R] (P : R[X])
variable {P}
Lean source · statement
theorem etale (hP : P.Monic) (hirr : Irreducible (P.map (residue R)))
    (hsep : (P.map (residue R)).Separable) : Algebra.Etale R (AdjoinRoot P)
theorem

exists_residues

L131 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq.IsLocalRing.ResidueExtImpl.exists_residues
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq
universe u
open _root_.Polynomial
open _root_.IsLocalRing
namespace IsLocalRing
open _root_.IsLocalRing
namespace ResidueExtImpl
open _root_.IsLocalRing
section AdjoinRoot
variable {R : Type u} [CommRing R] [IsLocalRing R] (P : R[X])
variable {P}
Lean source · statement
theorem exists_residues {n : ℕ}
    (y : Fin (n + 1) → AdjoinRoot (P.map (residue R))) (hy : Function.Injective y) :
    ∃ x : Fin (n + 1) → AdjoinRoot P, ∀ i j, x i - x j ∈ m0 P → i = j
theorem

exists_irreducible_card_gt

L150 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq.IsLocalRing.ResidueExtImpl.exists_irreducible_card_gt
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq
universe u
open _root_.Polynomial
open _root_.IsLocalRing
namespace IsLocalRing
open _root_.IsLocalRing
namespace ResidueExtImpl
open _root_.IsLocalRing
section Field
variable (k : Type u) [Field k] [Fintype k]
omit [Fintype k] in
Lean source · statement
theorem exists_irreducible_card_gt [Finite k] (n : ℕ) :
    ∃ Pb : k[X], Pb.Monic ∧ Irreducible Pb ∧ Pb.Separable ∧
      ∃ y : Fin (n + 1) → AdjoinRoot Pb, Function.Injective y
theorem

main

L194 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq.IsLocalRing.ResidueExtImpl.main
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq
universe u
open _root_.Polynomial
open _root_.IsLocalRing
namespace IsLocalRing
open _root_.IsLocalRing
namespace ResidueExtImpl
open _root_.IsLocalRing
Lean source · statement
theorem main (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (n : ℕ) :
    ∃ (R₀ : Type u) (_ : CommRing R₀) (_ : Algebra R R₀) (_ : Module.Finite R R₀)
      (_ : Algebra.Etale R R₀) (_ : Module.FaithfullyFlat R R₀) (_ : IsLocalRing R₀) (_ :
        IsNoetherianRing R₀)
      (_ : IsLocalHom (algebraMap R R₀)) (x : Fin (n + 1) → R₀),
      ∀ i j, x i - x j ∈ IsLocalRing.maximalIdeal R₀ → i = j
theorem

exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq

L235 ↗
IsLocalRing.exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq
universe u
open _root_.Polynomial
open _root_.IsLocalRing
Lean source · statement
theorem
  _root_.IsLocalRing.exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (n : ℕ) :
    ∃ (R₀ : Type u) (_ : CommRing R₀) (_ : Algebra R R₀) (_ : Module.Finite R R₀)
      (_ : Algebra.Etale R R₀) (_ : Module.FaithfullyFlat R R₀) (_ : IsLocalRing R₀) (_ :
        IsNoetherianRing R₀)
      (_ : IsLocalHom (algebraMap R R₀)) (x : Fin (n + 1) → R₀),
      ∀ i j, x i - x j ∈ IsLocalRing.maximalIdeal R₀ → i = j

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