Module

PolynomialCRT.lean

Nyll.ValuedFieldTheory.Valuation.Completion.PolynomialCRT

3 declarations indexed from sourceView source ↗

Module documentation

Polynomial Chinese remainder equivalence

This is the algebraic core of tensor-product decompositions. A squarefree factorization of the base-changed primitive polynomial gives the canonical product of its simple factor algebras.

Imports2

Mathlib.RingTheory.AdjoinRoot
Mathlib.RingTheory.Ideal.Quotient.Operations

Imported by2

def

quotientInfAlgEquivPiQuotient

L30 ↗

ValuationTheory.Completion.quotientInfAlgEquivPiQuotient

Documentation

The Chinese remainder ring equivalence is an algebra equivalence over any coefficient ring acting on the ambient commutative ring.

Source context 6 commands

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

noncomputable section
namespace ValuationTheory
namespace Completion
universe u v
open scoped Polynomial
open Function

Lean source · full declaration

def quotientInfAlgEquivPiQuotient
    {R A : Type*} [CommRing R] [CommRing A] [Algebra R A]
    {ι : Type*} [Finite ι]
    (I : ι → Ideal A) (hI : Pairwise (IsCoprime on I)) :
    (A ⧸ ⨅ i, I i) ≃ₐ[R] ∀ i, A ⧸ I i where
  __ := Ideal.quotientInfRingEquivPiQuotient I hI
  commutes' r := by
    ext i
    rfl

def

adjoinRootProdEquivPi

L43 ↗

ValuationTheory.Completion.adjoinRootProdEquivPi

Documentation

Chinese remainder equivalence for a finite family of pairwise coprime polynomials. It is canonical: every polynomial class is sent to the family of the same class modulo each factor.

Source context 6 commands

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

noncomputable section
namespace ValuationTheory
namespace Completion
universe u v
open scoped Polynomial
open Function

Lean source · statement

def adjoinRootProdEquivPi
    {F : Type u} [Field F] {ι : Type v} [Fintype ι]
    (f : ι → F[X])
    (hf : ∀ i j, i ≠ j → IsCoprime (f i) (f j)) :
    AdjoinRoot (∏ i, f i) ≃ₐ[F] ∀ i, AdjoinRoot (f i)

theorem

adjoinRootProdEquivPi_mk

L63 ↗

ValuationTheory.Completion.adjoinRootProdEquivPi_mk

Documentation

The product decomposition of an adjoined-root algebra evaluates representatives coordinatewise.

Source context 6 commands

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

noncomputable section
namespace ValuationTheory
namespace Completion
universe u v
open scoped Polynomial
open Function

Lean source · statement

theorem adjoinRootProdEquivPi_mk
    {F : Type u} [Field F] {ι : Type v} [Fintype ι]
    (f : ι → F[X])
    (hf : ∀ i j, i ≠ j → IsCoprime (f i) (f j))
    (g : F[X]) (i : ι) :
    adjoinRootProdEquivPi f hf (AdjoinRoot.mk (∏ i, f i) g) i =
      AdjoinRoot.mk (f i) g

Module documentation

Polynomial Chinese remainder equivalence

Declarations

quotientInfAlgEquivPiQuotient

adjoinRootProdEquivPi

adjoinRootProdEquivPi_mk