FieldFibers.lean

1 import PaperXII.ModuleSupport
2 import Mathlib.RingTheory.LocalRing.Module
3 import Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
4 import Mathlib.LinearAlgebra.TensorProduct.Tower
5 
6 /-! Paper XII, Theorem 7.4. The fiber is an actual tensor product. -/
7 namespace PaperXII.FieldFibers
8 
9 open scoped TensorProduct
10 
11 variable {R E M : Type*} [CommRing R] [Field E]
12     [AddCommGroup M] [Module R M]
13 
14 /-- The prime associated with a field-valued point. -/
15 def pointPrime (x : R →+* E) : PrimeSpectrum R :=
16   ⟨RingHom.ker x, RingHom.ker_isPrime x⟩
17 
18 /-- Every element outside the point kernel maps to a unit in the field. -/
19 theorem primeCompl_maps_to_units (x : R →+* E) :
20     (pointPrime x).asIdeal.primeCompl ≤ (IsUnit.submonoid E).comap x := by
21   intro r hr
22   change IsUnit (x r)
23   apply isUnit_iff_ne_zero.mpr
24   exact hr
25 
26 /-- A field-valued point extends to the residue field at its exact kernel. -/
27 noncomputable def residueFieldLift (x : R →+* E) :
28     (pointPrime x).asIdeal.ResidueField →+* E :=
29   Ideal.ResidueField.lift _ x le_rfl (primeCompl_maps_to_units x)
30 
31 /-- The constructed residue-field embedding factors the original point. -/
32 theorem residueFieldLift_comp (x : R →+* E) :
33     (residueFieldLift x).comp (algebraMap R (pointPrime x).asIdeal.ResidueField) = x := by
34   ext r
35   exact Ideal.ResidueField.lift_algebraMap (pointPrime x).asIdeal x le_rfl
36     (primeCompl_maps_to_units x) r
37 
38 /-- The field-fiber criterion in algebra-instance form. -/
39 theorem nontrivial_tensor_iff_support [Algebra R E] [Module.Finite R M] :
40     Nontrivial (E ⊗[R] M) ↔ pointPrime (algebraMap R E) ∈ Module.support R M := by
41   let p := pointPrime (algebraMap R E)
42   let K := p.asIdeal.ResidueField
43   let f : K →+* E := residueFieldLift (algebraMap R E)
44   let : Algebra K E := f.toAlgebra
45   let : IsScalarTower R K E := IsScalarTower.of_algebraMap_eq' (residueFieldLift_comp _).symm
46   let e := TensorProduct.AlgebraTensorModule.cancelBaseChange R K E E M
47   rw [← e.nontrivial_congr, Module.FaithfullyFlat.nontrivial_tensorProduct_iff_right K E]
48   exact (Module.mem_support_iff_nontrivial_residueField_tensorProduct p).symm
49 
50 /-- Theorem 7.4 for an arbitrary explicitly supplied ring homomorphism. -/
51 theorem nontrivial_fiber_iff_support (x : R →+* E) [Module.Finite R M] :
52     let : Algebra R E := x.toAlgebra
53     Nontrivial (E ⊗[R] M) ↔ pointPrime x ∈ Module.support R M := by
54   let : Algebra R E := x.toAlgebra
55   exact nontrivial_tensor_iff_support
56 
57 /-- The source tensor order M ⊗ E gives the same field-fiber criterion. -/
58 theorem nontrivial_right_fiber_iff_support (x : R →+* E) [Module.Finite R M] :
59     letI : Algebra R E := x.toAlgebra
60     Nontrivial (M ⊗[R] E) ↔ pointPrime x ∈ Module.support R M := by
61   let : Algebra R E := x.toAlgebra
62   exact (TensorProduct.comm R M E).nontrivial_congr.trans
63     (nontrivial_fiber_iff_support x)
64 
65 /-- Under full support, every actual field-valued fiber is nonzero. -/
66 theorem nontrivial_fiber_of_fullSupport (x : R →+* E) [Module.Finite R M]
67     (h : ModuleSupport.FullSupport R M) :
68     letI : Algebra R E := x.toAlgebra
69     Nontrivial (E ⊗[R] M) :=
70   (nontrivial_fiber_iff_support x).mpr
71     ((ModuleSupport.fullSupport_iff_localizations R M).mp h _)
72 
73 end PaperXII.FieldFibers

Back to source controls