MonicResidueAlgebra.lean

1 import Mathlib.RingTheory.AdjoinRoot
2 import Mathlib.Algebra.Polynomial.Eval.Irreducible
3 import Mathlib.RingTheory.LocalRing.Quotient
4 import Mathlib.RingTheory.Ideal.GoingUp
5 import Mathlib.Tactic
6 
7 /-! Monic lifts with irreducible residue polynomial give finite free local
8 algebras with their literal special fiber. No ambient field is supplied. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.MonicResidueAlgebra
12 open Polynomial IsLocalRing
13 variable {R : Type*} [CommRing R] [IsLocalRing R]
14 variable (f : R[X]) [hm : Fact f.Monic]
15 variable [hi : Fact (Irreducible (f.map (residue R)))]
16 
17 abbrev specialIdeal : Ideal (AdjoinRoot f) :=
18   (maximalIdeal R).map (algebraMap R (AdjoinRoot f))
19 
20 instance finite : Module.Finite R (AdjoinRoot f) := hm.out.finite_adjoinRoot
21 instance free : Module.Free R (AdjoinRoot f) := hm.out.free_adjoinRoot
22 
23 /-- The base special fiber is the actual residue polynomial algebra. -/
24 def specialFiberEquiv :
25     (AdjoinRoot f ⧸ specialIdeal f) ≃ₐ[R] AdjoinRoot (f.map (residue R)) :=
26   AdjoinRoot.quotEquivQuotMap f (maximalIdeal R)
27 
28 omit hm in
29 theorem specialIdeal_maximal : (specialIdeal f).IsMaximal := by
30   apply Ideal.Quotient.maximal_of_isField
31   exact (specialFiberEquiv f).toRingEquiv.toMulEquiv.isField (Field.toIsField _)
32 
33 /-- All maximal ideals lie above the base maximal ideal; the special fiber is a field. -/
34 instance localRing : IsLocalRing (AdjoinRoot f) := by
35   let := AdjoinRoot.isIntegral_of_monic hm.out
36   apply IsLocalRing.of_unique_max_ideal
37   refine ⟨specialIdeal f, specialIdeal_maximal f, ?_⟩
38   intro M hM
39   let : M.IsMaximal := hM
40   have hcomap : M.comap (algebraMap R (AdjoinRoot f)) = maximalIdeal R :=
41     IsLocalRing.eq_maximalIdeal (Ideal.isMaximal_comap_of_isIntegral_of_isMaximal M)
42   have hle : specialIdeal f ≤ M := by
43     rw [specialIdeal, Ideal.map_le_iff_le_comap, hcomap]
44   exact ((specialIdeal_maximal f).eq_of_le hM.ne_top hle).symm
45 
46 theorem maximalIdeal_eq : maximalIdeal (AdjoinRoot f) = specialIdeal f :=
47   (IsLocalRing.eq_maximalIdeal (specialIdeal_maximal f)).symm
48 
49 def residueEquiv : ResidueField (AdjoinRoot f) ≃+* AdjoinRoot (f.map (residue R)) :=
50   (Ideal.quotEquivOfEq (maximalIdeal_eq f)).trans (specialFiberEquiv f).toRingEquiv
51 
52 omit hi in
53 theorem rank : Module.finrank R (AdjoinRoot f) = f.natDegree := by
54   simpa using Module.finrank_eq_card_basis (AdjoinRoot.powerBasis' hm.out).basis
55 
56 theorem degree_pos : 0 < f.degree := by
57   rw [← hm.out.degree_map (residue R)]
58   exact Polynomial.degree_pos_of_irreducible hi.out
59 
60 instance localHom : IsLocalHom (algebraMap R (AdjoinRoot f)) :=
61   AdjoinRoot.isLocalHom_of_monic_of_degree_pos hm.out (degree_pos f)
62 
63 theorem residueEquiv_mk (p : R[X]) :
64     residueEquiv f (residue (AdjoinRoot f) (AdjoinRoot.mk f p)) =
65       AdjoinRoot.mk (f.map (residue R)) (p.map (residue R)) := by
66   change (specialFiberEquiv f).toRingEquiv
67     ((Ideal.quotEquivOfEq (maximalIdeal_eq f))
68       (Ideal.Quotient.mk _ (AdjoinRoot.mk f p))) = _
69   rw [Ideal.quotEquivOfEq_mk]
70   exact AdjoinRoot.quotEquivQuotMap_apply_mk f p (maximalIdeal R)
71 
72 def residueAlgebraEquiv :
73     ResidueField (AdjoinRoot f) ≃ₐ[ResidueField R] AdjoinRoot (f.map (residue R)) :=
74   { residueEquiv f with
75     commutes' := fun a => by
76       obtain ⟨r, rfl⟩ := residue_surjective a
77       change residueEquiv f (residue (AdjoinRoot f) (AdjoinRoot.mk f (C r))) = _
78       rw [residueEquiv_mk, Polynomial.map_C]
79       rfl }
80 
81 theorem residue_rank :
82     Module.finrank (ResidueField R) (ResidueField (AdjoinRoot f)) = f.natDegree := by
83   rw [(residueAlgebraEquiv f).toLinearEquiv.finrank_eq]
84   simpa [hm.out.natDegree_map] using
85     Module.finrank_eq_card_basis (AdjoinRoot.powerBasis' (hm.out.map (residue R))).basis
86 
87 end PaperXI.MonicResidueAlgebra

Back to source controls