EtaleFundamentalGroups.tensorProduct_map_maximalIdeal_isMaximal_of_residueFieldMap_bijective
In a closed-point-preserving faithfully flat local base change, the extension of the target maximal ideal to the tensor product is maximal.
Surjectivity onto the quotient is proved directly: modulo the extended target maximal ideal, every coefficient in R' may be replaced by a lift from R, because the residue-field map is surjective and the discrepancy belongs to the extended source maximal ideal.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uR' uSLean source · full declaration
theorem tensorProduct_map_maximalIdeal_isMaximal_of_residueFieldMap_bijective
{R : Type uR} {R' : Type uR'} {S : Type uS}
[CommRing R] [CommRing R'] [CommRing S]
[IsLocalRing R] [IsLocalRing R'] [IsLocalRing S]
[Algebra R R'] [Algebra R S]
[IsLocalHom (algebraMap R R')] [IsLocalHom (algebraMap R S)]
[Module.FaithfullyFlat R R']
(hmax : (IsLocalRing.maximalIdeal R).map (algebraMap R R') =
IsLocalRing.maximalIdeal R')
(hres : Function.Bijective
(IsLocalRing.ResidueField.map (algebraMap R R'))) :
let T := R' ⊗[R] S
letI : Algebra S T := Algebra.TensorProduct.rightAlgebra
((IsLocalRing.maximalIdeal S).map (algebraMap S T)).IsMaximal := by
let T := R' ⊗[R] S
let : Algebra S T := Algebra.TensorProduct.rightAlgebra
let : IsScalarTower R S T :=
Algebra.TensorProduct.right_isScalarTower
let : Module.FaithfullyFlat S T :=
Module.FaithfullyFlat.of_linearEquiv
(R := S) (M := S ⊗[R] R')
(Algebra.TensorProduct.commRight R S R').symm.toLinearEquiv
let p := IsLocalRing.maximalIdeal R
let q := IsLocalRing.maximalIdeal S
let q' := q.map (algebraMap S T)
let g : S →+* T ⧸ q' :=
(Ideal.Quotient.mk q').comp (algebraMap S T)
have hpq : p.map (algebraMap R S) ≤ q := by
exact IsLocalRing.map_maximalIdeal_le (algebraMap R S)
have hsurj : Function.Surjective g := by
intro z
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective z
induction x using TensorProduct.inductionOn with
| tmul r' s =>
obtain ⟨k, hk⟩ := hres.2 (IsLocalRing.residue R' r')
obtain ⟨r, hr⟩ := IsLocalRing.residue_surjective k
let d : R' := r' - algebraMap R R' r
have hdzero : IsLocalRing.residue R' d = 0 := by
rw [map_sub,
← IsLocalRing.ResidueField.map_residue
(algebraMap R R') r,
hr, hk, sub_self]
have hdmax : d ∈ IsLocalRing.maximalIdeal R' :=
(IsLocalRing.residue_eq_zero_iff d).mp hdzero
have hdpmap : d ∈ p.map (algebraMap R R') := by
rw [hmax]
exact hdmax
have hdT : algebraMap R' T d ∈ q' := by
have hdT' : algebraMap R' T d ∈
(p.map (algebraMap R R')).map (algebraMap R' T) :=
Ideal.mem_map_of_mem (algebraMap R' T) hdpmap
have hpT : p.map (algebraMap R T) ≤ q' := by
calc
p.map (algebraMap R T) =
(p.map (algebraMap R S)).map (algebraMap S T) := by
rw [Ideal.map_map, IsScalarTower.algebraMap_eq R S T]
_ ≤ q.map (algebraMap S T) := Ideal.map_mono hpq
_ = q' := rfl
apply hpT
simpa only [Ideal.map_map,
IsScalarTower.algebraMap_eq R R' T] using hdT'
have hdiff :
r' ⊗ₜ[R] s -
(1 ⊗ₜ[R] (algebraMap R S r * s) : T) ∈ q' := by
have hmul : algebraMap R' T d * algebraMap S T s ∈ q' :=
q'.mul_mem_right (algebraMap S T s) hdT
have hfirst :
algebraMap R' T r' * algebraMap S T s =
(r' ⊗ₜ[R] s : T) := by
rw [Algebra.TensorProduct.algebraMap_apply,
Algebra.algebraMap_self_apply,
Algebra.TensorProduct.right_algebraMap_apply,
Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]
have hsecond :
algebraMap R' T (algebraMap R R' r) *
algebraMap S T s =
(1 ⊗ₜ[R] (algebraMap R S r * s) : T) := by
rw [← IsScalarTower.algebraMap_apply R R' T,
IsScalarTower.algebraMap_apply R S T,
Algebra.TensorProduct.right_algebraMap_apply,
Algebra.TensorProduct.right_algebraMap_apply,
Algebra.TensorProduct.tmul_mul_tmul, one_mul]
simpa only [d, map_sub, sub_mul, hfirst, hsecond] using hmul
refine ⟨algebraMap R S r * s, ?_⟩
apply Ideal.Quotient.eq.2
change algebraMap S T (algebraMap R S r * s) -
(r' ⊗ₜ[R] s : T) ∈ q'
rw [Algebra.TensorProduct.right_algebraMap_apply, ← neg_sub]
exact q'.neg_mem hdiff
| add x y hx hy =>
obtain ⟨sx, hsx⟩ := hx
obtain ⟨sy, hsy⟩ := hy
refine ⟨sx + sy, ?_⟩
change g (sx + sy) =
Ideal.Quotient.mk q' (x + y)
rw [map_add, map_add, hsx, hsy]
have hker : RingHom.ker g = q := by
ext s
rw [RingHom.mem_ker]
change Ideal.Quotient.mk q' (algebraMap S T s) = 0 ↔ s ∈ q
rw [Ideal.Quotient.eq_zero_iff_mem]
simpa [q'] using
(show s ∈ (q.map (algebraMap S T)).comap
(algebraMap S T) ↔ s ∈ q by
rw [Ideal.comap_map_eq_self_of_faithfullyFlat])
let : q.IsMaximal := IsLocalRing.maximalIdeal.isMaximal S
let : Field (S ⧸ q) := Ideal.Quotient.field q
have hfieldKer : IsField (S ⧸ RingHom.ker g) := by
rw [hker]
exact Field.toIsField (S ⧸ q)
have hfieldQuot : IsField (T ⧸ q') :=
(RingHom.quotientKerEquivOfSurjective hsurj).symm.toMulEquiv.isField
hfieldKer
exact (Ideal.Quotient.maximal_ideal_iff_isField_quotient q').2
hfieldQuot