Documentation

Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Residue field of primes in polynomial algebras #

Main results #

source
noncomputable def Polynomial.residueFieldMapCAlgEquiv {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] (J : Ideal (Polynomial R)) [J.IsPrime] [J.LiesOver I] [Algebra (Localization.AtPrime I) (Localization.AtPrime J)] [IsScalarTower R (Localization.AtPrime I) (Localization.AtPrime J)] (hJ : J = Ideal.map C I) :
J.ResidueField ≃ₐ[I.ResidueField] RatFunc I.ResidueField

κ(I[X]) ≃ₐ[κ(I)] κ(I)(X).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Polynomial.residueFieldMapCAlgEquiv_algebraMap {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] (J : Ideal (Polynomial R)) [J.IsPrime] [J.LiesOver I] [Algebra (Localization.AtPrime I) (Localization.AtPrime J)] [IsScalarTower R (Localization.AtPrime I) (Localization.AtPrime J)] (hJ : J = Ideal.map C I) (p : Polynomial R) :
    (residueFieldMapCAlgEquiv I J hJ) ((algebraMap (Polynomial R) J.ResidueField) p) = (algebraMap (Polynomial I.ResidueField) (RatFunc I.ResidueField)) (map (algebraMap R I.ResidueField) p)
    source
    @[simp]
    theorem Polynomial.residueFieldMapCAlgEquiv_symm_C {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] (J : Ideal (Polynomial R)) [J.IsPrime] [J.LiesOver I] [Algebra (Localization.AtPrime I) (Localization.AtPrime J)] [IsScalarTower R (Localization.AtPrime I) (Localization.AtPrime J)] (hJ : J = Ideal.map C I) (r : I.ResidueField) :
    (residueFieldMapCAlgEquiv I J hJ).symm (RatFunc.C r) = (algebraMap I.ResidueField J.ResidueField) r
    source
    @[simp]
    theorem Polynomial.residueFieldMapCAlgEquiv_symm_X {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] (J : Ideal (Polynomial R)) [J.IsPrime] [J.LiesOver I] [Algebra (Localization.AtPrime I) (Localization.AtPrime J)] [IsScalarTower R (Localization.AtPrime I) (Localization.AtPrime J)] (hJ : J = Ideal.map C I) :
    (residueFieldMapCAlgEquiv I J hJ).symm RatFunc.X = (algebraMap (Polynomial R) J.ResidueField) X
    source
    noncomputable def Polynomial.fiberEquivQuotient {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (f : Polynomial R →ₐ[R] S) (hf : Function.Surjective ⇑f) (p : Ideal R) [p.IsPrime] :
    p.Fiber S ≃ₐ[p.ResidueField] Polynomial p.ResidueField ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)

    κ(p) ⊗[R] (R[X] ⧸ I) = κ(p)[X] / I

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Polynomial.fiberEquivQuotient_tmul {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (f : Polynomial R →ₐ[R] S) (hf : Function.Surjective ⇑f) (p : Ideal R) [p.IsPrime] (a : p.ResidueField) (b : Polynomial R) :
      (fiberEquivQuotient f hf p) (a ⊗ₜ[R] f b) = (Ideal.Quotient.mk (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))) (C a * map (algebraMap R p.ResidueField) b)
      source
      theorem Ideal.exists_mem_span_singleton_map_residueField_eq {R : Type u_1} [CommRing R] (P : Ideal R) [P.IsPrime] (I : Ideal (Polynomial R)) :
      ∃ p ∈ I, span {Polynomial.map (algebraMap R P.ResidueField) p} = map (Polynomial.mapRingHom (algebraMap R P.ResidueField)) I

      Given a prime P of R and an ideal I of R[X], the image of I in κ(P)[X] is generated by some p ∈ I (basically because κ(P)[X] is a PID).