EtaleFundamentalGroups.exists_activeBranch_eq_of_heightOnePrime_mem_boundaryProduct
A height-one prime containing the product of a finite family of prime elements is the principal prime generated by one of the factors occurring in that product. This is the branch-selection core which does not require regularity of the other branch quotients.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
universe uLean source · statement
theorem exists_activeBranch_eq_of_heightOnePrime_mem_boundaryProduct
{R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
{d r : ℕ} {t : Fin d → R}
(hprime : ∀ i : Fin d, i.1 < r → Prime (t i))
(q : Ideal R) [q.IsPrime] (hqheight : q.height = 1)
(hprod : boundaryProduct t r ∈ q) :
∃ i : Fin d, i.1 < r ∧ q = Ideal.span ({t i} : Set R)