|
| 1 | +/- |
| 2 | +Copyright (c) 2019 Kenny Lau. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Kenny Lau |
| 5 | +-/ |
| 6 | +import Mathlib.RingTheory.IntegralClosure.Algebra.Defs |
| 7 | +import Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic |
| 8 | +import Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap |
| 9 | + |
| 10 | +#align_import ring_theory.integral_closure from "leanprover-community/mathlib"@"641b6a82006416ec431b2987b354af9311fed4f2" |
| 11 | + |
| 12 | +/-! |
| 13 | +# Integral closure of a subring. |
| 14 | +
|
| 15 | +Let `A` be an `R`-algebra. We prove that integral elements form a sub-`R`-algebra of `A`. |
| 16 | +
|
| 17 | +## Main definitions |
| 18 | +
|
| 19 | +Let `R` be a `CommRing` and let `A` be an R-algebra. |
| 20 | +
|
| 21 | +* `integralClosure R A` : the integral closure of `R` in an `R`-algebra `A`. |
| 22 | +-/ |
| 23 | + |
| 24 | + |
| 25 | +open Polynomial Submodule |
| 26 | + |
| 27 | +section |
| 28 | + |
| 29 | +variable {R A B S : Type*} |
| 30 | +variable [CommRing R] [CommRing A] [Ring B] [CommRing S] |
| 31 | +variable [Algebra R A] [Algebra R B] (f : R →+* S) |
| 32 | + |
| 33 | +section |
| 34 | + |
| 35 | +variable {A B : Type*} [Ring A] [Ring B] [Algebra R A] [Algebra R B] |
| 36 | +variable (f : A →ₐ[R] B) (hf : Function.Injective f) |
| 37 | + |
| 38 | +end |
| 39 | + |
| 40 | +instance Module.End.isIntegral {M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M] : |
| 41 | + Algebra.IsIntegral R (Module.End R M) := |
| 42 | + ⟨LinearMap.exists_monic_and_aeval_eq_zero R⟩ |
| 43 | +#align module.End.is_integral Module.End.isIntegral |
| 44 | + |
| 45 | +variable (R) |
| 46 | +theorem IsIntegral.of_finite [Module.Finite R B] (x : B) : IsIntegral R x := |
| 47 | + (isIntegral_algHom_iff (Algebra.lmul R B) Algebra.lmul_injective).mp |
| 48 | + (Algebra.IsIntegral.isIntegral _) |
| 49 | + |
| 50 | +variable (B) |
| 51 | +instance Algebra.IsIntegral.of_finite [Module.Finite R B] : Algebra.IsIntegral R B := |
| 52 | + ⟨.of_finite R⟩ |
| 53 | +#align algebra.is_integral.of_finite Algebra.IsIntegral.of_finite |
| 54 | + |
| 55 | +variable {R B} |
| 56 | + |
| 57 | +/-- If `S` is a sub-`R`-algebra of `A` and `S` is finitely-generated as an `R`-module, |
| 58 | + then all elements of `S` are integral over `R`. -/ |
| 59 | +theorem IsIntegral.of_mem_of_fg {A} [Ring A] [Algebra R A] (S : Subalgebra R A) |
| 60 | + (HS : S.toSubmodule.FG) (x : A) (hx : x ∈ S) : IsIntegral R x := |
| 61 | + have : Module.Finite R S := ⟨(fg_top _).mpr HS⟩ |
| 62 | + (isIntegral_algHom_iff S.val Subtype.val_injective).mpr (.of_finite R (⟨x, hx⟩ : S)) |
| 63 | +#align is_integral_of_mem_of_fg IsIntegral.of_mem_of_fg |
| 64 | + |
| 65 | +theorem RingHom.IsIntegralElem.of_mem_closure {x y z : S} (hx : f.IsIntegralElem x) |
| 66 | + (hy : f.IsIntegralElem y) (hz : z ∈ Subring.closure ({x, y} : Set S)) : f.IsIntegralElem z := by |
| 67 | + letI : Algebra R S := f.toAlgebra |
| 68 | + have := (IsIntegral.fg_adjoin_singleton hx).mul (IsIntegral.fg_adjoin_singleton hy) |
| 69 | + rw [← Algebra.adjoin_union_coe_submodule, Set.singleton_union] at this |
| 70 | + exact |
| 71 | + IsIntegral.of_mem_of_fg (Algebra.adjoin R {x, y}) this z |
| 72 | + (Algebra.mem_adjoin_iff.2 <| Subring.closure_mono Set.subset_union_right hz) |
| 73 | +#align ring_hom.is_integral_of_mem_closure RingHom.IsIntegralElem.of_mem_closure |
| 74 | + |
| 75 | +nonrec theorem IsIntegral.of_mem_closure {x y z : A} (hx : IsIntegral R x) (hy : IsIntegral R y) |
| 76 | + (hz : z ∈ Subring.closure ({x, y} : Set A)) : IsIntegral R z := |
| 77 | + hx.of_mem_closure (algebraMap R A) hy hz |
| 78 | +#align is_integral_of_mem_closure IsIntegral.of_mem_closure |
| 79 | + |
| 80 | +variable (f : R →+* B) |
| 81 | + |
| 82 | +theorem RingHom.IsIntegralElem.add (f : R →+* S) {x y : S} |
| 83 | + (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) : |
| 84 | + f.IsIntegralElem (x + y) := |
| 85 | + hx.of_mem_closure f hy <| |
| 86 | + Subring.add_mem _ (Subring.subset_closure (Or.inl rfl)) (Subring.subset_closure (Or.inr rfl)) |
| 87 | +#align ring_hom.is_integral_add RingHom.IsIntegralElem.add |
| 88 | + |
| 89 | +nonrec theorem IsIntegral.add {x y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) : |
| 90 | + IsIntegral R (x + y) := |
| 91 | + hx.add (algebraMap R A) hy |
| 92 | +#align is_integral_add IsIntegral.add |
| 93 | + |
| 94 | +variable (f : R →+* S) |
| 95 | + |
| 96 | +-- can be generalized to noncommutative S. |
| 97 | +theorem RingHom.IsIntegralElem.neg {x : S} (hx : f.IsIntegralElem x) : f.IsIntegralElem (-x) := |
| 98 | + hx.of_mem_closure f hx (Subring.neg_mem _ (Subring.subset_closure (Or.inl rfl))) |
| 99 | +#align ring_hom.is_integral_neg RingHom.IsIntegralElem.neg |
| 100 | + |
| 101 | +theorem IsIntegral.neg {x : B} (hx : IsIntegral R x) : IsIntegral R (-x) := |
| 102 | + .of_mem_of_fg _ hx.fg_adjoin_singleton _ (Subalgebra.neg_mem _ <| Algebra.subset_adjoin rfl) |
| 103 | +#align is_integral_neg IsIntegral.neg |
| 104 | + |
| 105 | +theorem RingHom.IsIntegralElem.sub {x y : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) : |
| 106 | + f.IsIntegralElem (x - y) := by |
| 107 | + simpa only [sub_eq_add_neg] using hx.add f (hy.neg f) |
| 108 | +#align ring_hom.is_integral_sub RingHom.IsIntegralElem.sub |
| 109 | + |
| 110 | +nonrec theorem IsIntegral.sub {x y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) : |
| 111 | + IsIntegral R (x - y) := |
| 112 | + hx.sub (algebraMap R A) hy |
| 113 | +#align is_integral_sub IsIntegral.sub |
| 114 | + |
| 115 | +theorem RingHom.IsIntegralElem.mul {x y : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) : |
| 116 | + f.IsIntegralElem (x * y) := |
| 117 | + hx.of_mem_closure f hy |
| 118 | + (Subring.mul_mem _ (Subring.subset_closure (Or.inl rfl)) (Subring.subset_closure (Or.inr rfl))) |
| 119 | +#align ring_hom.is_integral_mul RingHom.IsIntegralElem.mul |
| 120 | + |
| 121 | +nonrec theorem IsIntegral.mul {x y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) : |
| 122 | + IsIntegral R (x * y) := |
| 123 | + hx.mul (algebraMap R A) hy |
| 124 | +#align is_integral_mul IsIntegral.mul |
| 125 | + |
| 126 | +theorem IsIntegral.smul {R} [CommSemiring R] [CommRing S] [Algebra R B] [Algebra S B] [Algebra R S] |
| 127 | + [IsScalarTower R S B] {x : B} (r : R)(hx : IsIntegral S x) : IsIntegral S (r • x) := |
| 128 | + .of_mem_of_fg _ hx.fg_adjoin_singleton _ <| by |
| 129 | + rw [← algebraMap_smul S]; apply Subalgebra.smul_mem; exact Algebra.subset_adjoin rfl |
| 130 | +#align is_integral_smul IsIntegral.smul |
| 131 | + |
| 132 | +variable (R A) |
| 133 | + |
| 134 | +/-- The integral closure of `R` in an `R`-algebra `A`. -/ |
| 135 | +def integralClosure : Subalgebra R A where |
| 136 | + carrier := { r | IsIntegral R r } |
| 137 | + zero_mem' := isIntegral_zero |
| 138 | + one_mem' := isIntegral_one |
| 139 | + add_mem' := IsIntegral.add |
| 140 | + mul_mem' := IsIntegral.mul |
| 141 | + algebraMap_mem' _ := isIntegral_algebraMap |
| 142 | +#align integral_closure integralClosure |
| 143 | + |
| 144 | +end |
0 commit comments