LocalResidueRank.lean

1 import Mathlib.RingTheory.LocalRing.Etale
2 import Mathlib.RingTheory.LocalRing.Quotient
3 import Mathlib.RingTheory.Smooth.Fiber
4 import Mathlib.RingTheory.RamificationInertia.Ramification
5 import Mathlib.RingTheory.Unramified.LocalRing
6 
7 /-! An equal-rank residue fiber criterion for actual finite etale local algebras. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.LocalResidueRank
11 open IsLocalRing
12 variable (R S : Type*) [CommRing R] [CommRing S] [Algebra R S]
13 variable [IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)]
14 variable [Module.Finite R S] [Module.Free R S]
15 
16 set_option backward.inferInstanceAs.wrap.data false in
17 /-- When the finite free rank is already exhausted by the residue degree,
18 no nilpotent thickness remains in the special fiber. -/
19 theorem map_maximal_of_rank
20     (h : Module.finrank R S = Module.finrank (ResidueField R) (ResidueField S)) :
21     (maximalIdeal R).map (algebraMap R S) = maximalIdeal S := by
22   let J := (maximalIdeal R).map (algebraMap R S)
23   have hJ : J ≤ maximalIdeal S :=
24     ((local_hom_TFAE (algebraMap R S)).out 1 3 rfl rfl).mp inferInstance
25   let : Algebra (ResidueField R) (S ⧸ J) :=
26     (inferInstanceAs <| Algebra (R ⧸ maximalIdeal R) _)
27   let : IsScalarTower R (ResidueField R) (S ⧸ J) :=
28     (inferInstanceAs <| IsScalarTower R (R ⧸ maximalIdeal R) _)
29   let f : S ⧸ J →ₐ[ResidueField R] ResidueField S :=
30     { Ideal.Quotient.factor hJ with
31       commutes' := fun r => by
32         obtain ⟨r, rfl⟩ := residue_surjective r
33         rfl }
34   have hf : Function.Surjective f := Ideal.Quotient.factor_surjective hJ
35   have : Module.Finite (ResidueField R) (S ⧸ J) :=
36     Module.Finite.of_restrictScalars_finite R _ _
37   have heq : Module.finrank (ResidueField R) (S ⧸ J) =
38       Module.finrank (ResidueField R) (ResidueField S) := by
39     exact (IsLocalRing.finrank_quotient_map (R := R) (S := S)).trans h
40   have hi : Function.Injective f :=
41     (LinearMap.injective_iff_surjective_of_finrank_eq_finrank
42       (f := f.toLinearMap) heq).mpr hf
43   apply le_antisymm hJ
44   intro x hx
45   have hzero : f (Ideal.Quotient.mk J x) = f 0 := by
46     change residue S x = 0
47     simpa only [residue_eq_zero_iff] using hx
48   exact Ideal.Quotient.eq_zero_iff_mem.mp (hi hzero)
49 
50 /-- This is Mathlib's formal-unramified predicate, not a substitute definition. -/
51 theorem formallyUnramified [Algebra.IsSeparable (ResidueField R) (ResidueField S)]
52     (h : Module.finrank R S = Module.finrank (ResidueField R) (ResidueField S)) :
53     Algebra.FormallyUnramified R S := by
54   exact Algebra.FormallyUnramified.of_map_maximalIdeal (map_maximal_of_rank R S h)
55 
56 /-- Finite presentation and flatness yield the actual etale predicate. -/
57 theorem etale [Algebra.FinitePresentation R S]
58     [Algebra.IsSeparable (ResidueField R) (ResidueField S)]
59     (h : Module.finrank R S = Module.finrank (ResidueField R) (ResidueField S)) :
60     Algebra.Etale R S := by
61   let := formallyUnramified R S h
62   exact Algebra.Etale.of_formallyUnramified_of_flat
63 
64 /-- The criterion is an equivalence for finite free local algebras with
65 separable residue extension. -/
66 theorem etale_iff_rank_residue [Algebra.FinitePresentation R S]
67     [Algebra.IsSeparable (ResidueField R) (ResidueField S)] :
68     Algebra.Etale R S ↔
69       Module.finrank R S = Module.finrank (ResidueField R) (ResidueField S) := by
70   constructor
71   · intro h
72     let := h
73     exact IsLocalRing.finrank_eq_finrank_residueField
74   · exact etale R S
75 
76 /-- In particular the library's ramification index is one. -/
77 theorem ramificationIdx_one [Algebra.IsSeparable (ResidueField R) (ResidueField S)]
78     (h : Module.finrank R S = Module.finrank (ResidueField R) (ResidueField S)) :
79     (maximalIdeal S).ramificationIdx R = 1 := by
80   let := formallyUnramified R S h
81   exact Ideal.ramificationIdx_eq_one _ _
82 
83 end PaperXI.LocalResidueRank

Back to source controls