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: LetSbe a module-finiteR-algebra, andqa prime lying overp. We may construct an etaleR-algebraR'and a primePlying overpwithκ(P) = κ(p), such thatR' ⊗[R] S = A × Band there exists a unique prime inAlying overP. This prime will also lie overq.
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') ⋯))
:
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.
Instances For
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))
:
@[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)))
:
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₂)
:
theorem
Algebra.exists_etale_isIdempotentElem_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]
(q : Ideal S)
[q.IsPrime]
[q.LiesOver p]
:
∃ (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') ⋯) ∧ ∀ (P'' : Ideal (TensorProduct R R' S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
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.
The actual lemma is stated in terms of the idempotent element e = (1, 0).