Nyll.EtaleFundamentalGroups.FiniteEtale.ChosenPrime.Basic

Module documentation

A chosen prime below the étale factor of Tag 00UJ

Tag 00UJ chooses an étale base change and a prime in one finite idempotent factor above a specified prime q. For the one-point inertia argument we also have a smaller, height-one prime r ≤ q. Flat going down produces a prime below the chosen Tag 00UJ prime and the étale ramification-index comparison identifies its ramification index with that of r.

The right tensor-factor algebra and its flatness are proof-local. In particular this module does not register a second global algebra structure on a tensor product.

theorem

exists_etale_factor_prime_le_ramificationIdx_eq

L36 ↗

EtaleFundamentalGroups.exists_etale_factor_prime_le_ramificationIdx_eq

Documentation

Tag 00UJ may be chosen together with a prime above every specified smaller prime, without changing its ramification index.

The data before Q are the finite chosen factor supplied by Tag 00UJ. The additional prime Q is obtained by going down from P' along the right tensor-factor map. Its explicit contraction equality is the input expected by ramificationIdx_tensorProduct_eq_of_etale.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
universe u v

Lean source · statement

theorem exists_etale_factor_prime_le_ramificationIdx_eq
    {R : Type u} {B : Type v}
    [CommRing R] [CommRing B] [Algebra R B] [Algebra.FiniteType R B]
    (p : Ideal R) [p.IsPrime]
    (q : Ideal B) [q.IsPrime] [q.LiesOver p] [Algebra.QuasiFiniteAt R q]
    (r : Ideal B) [r.IsPrime] (hrq : r ≤ q) :
    ∃ (C : Type u) (_ : CommRing C) (_ : Algebra R C) (_ : Algebra.Etale R C)
      (P : Ideal C) (_ : P.IsPrime) (_ : P.LiesOver p)
      (e : TensorProduct R C B) (_ : IsIdempotentElem e)
      (P' Q : Ideal (TensorProduct R C B))
      (_ : P'.IsPrime) (_ : P'.LiesOver P) (_ : Q.IsPrime),
        P'.comap Algebra.TensorProduct.includeRight.toRingHom = q ∧
        Q ≤ P' ∧
        Q.comap Algebra.TensorProduct.includeRight.toRingHom = r ∧
        Q.ramificationIdx C = r.ramificationIdx R ∧
        e ∉ Q ∧
        e ∉ P' ∧
        Function.Bijective
          (Ideal.ResidueField.mapₐ p P (Algebra.ofId _ _) (P.over_def p)) ∧
        Module.Finite C (Localization.Away e) ∧
        ∀ P'' : Ideal (TensorProduct R C B),
          P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'

Module documentation

A chosen prime below the étale factor of Tag 00UJ

Declarations

exists_etale_factor_prime_le_ramificationIdx_eq