Etale local structure of finite maps

We construct etale neighborhoods that split fibers of finite algebras.

Main results

• Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq: Let S be a module-finite R-algebra, and q a prime lying over p. We may construct an etale R-algebra R' and a prime P lying over p with κ(P) = κ(p), such that R' ⊗[R] S = A × B and there exists a unique prime in A lying over P. This prime will also lie over q.

noncomputable def Ideal.fiberIsoOfBijectiveResidueField {R : Type u_1} {R' : Type u_2} {S : Type u_3} [CommRing R] [CommRing R'] [CommRing S] [Algebra R R'] [Algebra R S] {p : Ideal R} {q : Ideal R'} [p.IsPrime] [q.IsPrime] [q.LiesOver p] (H : Function.Bijective ⇑(ResidueField.mapₐ p q (Algebra.ofId R R') ⋯)) : ↑(q.primesOver (TensorProduct R R' S)) ≃o ↑(p.primesOver S)

If q is a prime of R' lying over p, a prime of R, such that κ(q) = κ(p), then the fiber of R' → R' ⊗[R] S over q is in bijection with the fiber of R → S over p.

Equations

• One or more equations did not get rendered due to their size.

theorem Ideal.comap_fiberIsoOfBijectiveResidueField_symm {R : Type u_1} {R' : Type u_2} {S : Type u_3} [CommRing R] [CommRing R'] [CommRing S] [Algebra R R'] [Algebra R S] {p : Ideal R} {q : Ideal R'} [p.IsPrime] [q.IsPrime] [q.LiesOver p] (H : Function.Bijective ⇑(ResidueField.mapₐ p q (Algebra.ofId R R') ⋯)) (Q : ↑(p.primesOver S)) : comap ↑Algebra.TensorProduct.includeRight ↑((fiberIsoOfBijectiveResidueField H).symm Q) = ↑Q

@[simp]

theorem Ideal.comap_fiberIsoOfBijectiveResidueField_apply {R : Type u_1} {R' : Type u_2} {S : Type u_3} [CommRing R] [CommRing R'] [CommRing S] [Algebra R R'] [Algebra R S] {p : Ideal R} {q : Ideal R'} [p.IsPrime] [q.IsPrime] [q.LiesOver p] (H : Function.Bijective ⇑(ResidueField.mapₐ p q (Algebra.ofId R R') ⋯)) (Q : ↑(q.primesOver (TensorProduct R R' S))) : ↑((fiberIsoOfBijectiveResidueField H) Q) = comap Algebra.TensorProduct.includeRight ↑Q

theorem Ideal.eq_of_comap_eq_comap_of_bijective_residueFieldMap {R : Type u_1} {R' : Type u_2} {S : Type u_3} [CommRing R] [CommRing R'] [CommRing S] [Algebra R R'] [Algebra R S] {p : Ideal R} {q : Ideal R'} [p.IsPrime] [q.IsPrime] [q.LiesOver p] (H : Function.Bijective ⇑(ResidueField.mapₐ p q (Algebra.ofId R R') ⋯)) (P₁ P₂ : Ideal (TensorProduct R R' S)) [P₁.IsPrime] [P₂.IsPrime] [P₁.LiesOver q] [P₂.LiesOver q] (H₂ : comap Algebra.TensorProduct.includeRight.toRingHom P₁ = comap Algebra.TensorProduct.includeRight.toRingHom P₂) : P₁ = P₂

theorem Localization.exists_finite_awayMapₐ_of_surjective_awayMapₐ {R : Type u} {S : Type v} {T : Type u_1} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra.FiniteType R T] [Algebra.IsIntegral R S] (f : S →ₐ[R] T) (g : S) (hg : Function.Surjective ⇑(awayMapₐ f g)) (p : Ideal R) [p.IsPrime] (hgp : IsUnit (1 ⊗ₜ[R] g)) : ∃ r ∉ p, (awayMapₐ (Algebra.ofId R T) r).Finite

Suppose f : S →ₐ[R] T is an R-algebra homomorphism with S integral and T of finite type, such that the induced map S[1/g] → T[1/g] is surjective for some g : S. Then for any prime p of R such that 1 ⊗ₜ g is invertible in κ(p) ⊗ S, there exists r ∉ p such that T[1/r] is finite over R[1/r].

theorem Algebra.exists_notMem_and_isIntegral_forall_mem_of_ne_of_liesOver {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p] [FiniteType R S] [QuasiFiniteAt R q] : ∃ s ∉ q, ∃ (hs : IsIntegral R s), (∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q') ∧ ∀ (q' : Ideal ↥(integralClosure R S)), q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q → q'.LiesOver p → ⟨s, hs⟩ ∈ q'

A variant of Ideal.exists_not_mem_forall_mem_of_ne_of_liesOver that also gives you control on the primes in the integral closure.

theorem Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [FiniteType R S] (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p] [QuasiFiniteAt R q] : ∃ (R' : Type u) (x : CommRing R') (x_1 : Algebra R R') (_ : Etale R R') (P : Ideal R') (x_3 : P.IsPrime) (x_4 : P.LiesOver p) (e : TensorProduct R R' S) (_ : IsIdempotentElem e) (e₀ : TensorProduct R R' ↥(integralClosure R S)) (_ : IsIdempotentElem e₀) (_ : (TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val) e₀ = e) (P' : Ideal (TensorProduct R R' S)) (_ : P'.IsPrime) (_ : P'.LiesOver P), Ideal.comap TensorProduct.includeRight.toRingHom P' = q ∧ e ∉ P' ∧ Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧ (∀ (P'' : Ideal (TensorProduct R R' ↥(integralClosure R S))), P''.IsPrime → P''.LiesOver P → e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val).toRingHom P') ∧ ∀ (P'' : Ideal (TensorProduct R R' S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'

theorem Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux₂ {R : Type u_2} {S : Type u_3} {R' : Type u_4} {R'' : Type u_5} [CommRing R] [CommRing S] [Algebra R S] [FiniteType R S] [CommRing R'] [Algebra R R'] [CommRing R''] [Algebra R R''] [Algebra R'' S] [Algebra.IsIntegral R R''] [IsScalarTower R R'' S] (q : Ideal S) (P : Ideal R') [P.IsPrime] (e : TensorProduct R R' S) (e₀ : TensorProduct R R' R'') (he₀ : IsIdempotentElem e₀) (he₀e : (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀ = e) (P' : Ideal (TensorProduct R R' S)) (hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q) (H : ∀ (P'' : Ideal (TensorProduct R R' R'')), P''.IsPrime → P''.LiesOver P → e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P') (g : R'') (hgq : (algebraMap R'' S) g ∉ q) (hg : Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g)) : ∃ f ∉ P, Module.Finite (Localization.Away f) (Localization.Away ((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)) e))

theorem Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [FiniteType R S] (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p] [QuasiFiniteAt R q] : ∃ (R' : Type u) (x : CommRing R') (x_1 : Algebra R R') (_ : Etale R R') (P : Ideal R') (x_3 : P.IsPrime) (x_4 : P.LiesOver p) (e : TensorProduct R R' S) (_ : IsIdempotentElem e) (P' : Ideal (TensorProduct R R' S)) (_ : P'.IsPrime) (_ : P'.LiesOver P), Ideal.comap TensorProduct.includeRight.toRingHom P' = q ∧ e ∉ P' ∧ Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧ Module.Finite R' (Localization.Away e) ∧ ∀ (P'' : Ideal (TensorProduct R R' S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'

Let S be a finite type R-algebra, and q a prime lying over p such that S is quasi-finite at q. We may construct an etale R-algebra R' and a prime P lying over p with κ(P) = κ(p), such that R' ⊗[R] S = A × B, A is finite as an R'-module, and there exists a unique prime in A lying over P. This prime will also lie over q.

The actual lemma is stated in terms of the idempotent element e = (1, 0).

theorem Algebra.exists_etale_completeOrthogonalIdempotents_forall_liesOver_eq {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S] (p : Ideal R) [p.IsPrime] : ∃ (R' : Type u) (x : CommRing R') (x_1 : Algebra R R') (_ : Etale R R') (P : Ideal R') (x_3 : P.IsPrime) (x_4 : P.LiesOver p) (n : ℕ) (e : Fin (n + 1) → TensorProduct R R' S) (_ : CompleteOrthogonalIdempotents e) (P' : Fin n → Ideal (TensorProduct R R' S)) (_ : ∀ (i : Fin n), (P' i).IsPrime) (_ : ∀ (i : Fin n), (P' i).LiesOver P), Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧ (∀ (i : Fin n), e i.castSucc ∉ P' i) ∧ ∀ (P'' : Ideal (TensorProduct R R' S)), P''.IsPrime → P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i

If S is finite over R, and p is a prime of R, then there exists an étale neighborhood (R', P) of p with κ(p) = κ(P) such that R' ⊗[R] S ≃ₐ[R'] R₁ × ... × Rₙ × A, each Rᵢ has a unique prime Pᵢ lying over P, and no other prime in R' ⊗[R] S lies over P.

This is merely an iterated application of exists_etale_isIdempotentElem_forall_liesOver_eq. This is weaker than the corresponding statement of stacks project (in particular we asked for Module.Finite instead of quasi finite when localized at p, so that we don't need to keep track of this when passing to quotients and tensor products), and the only reason is that the corresponding stronger statement is even harder to state and even more annoying to prove.