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).