Theorems · Theorem · commutative algebra

Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux

∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Algebra.FiniteType R S]
  (p : Ideal R) [inst_4 : p.IsPrime] (q : Ideal S) [inst_5 : q.IsPrime] [q.LiesOver p] [Algebra.QuasiFiniteAt R q],
  ∃ R' x x_1,
    ∃ (_ : Algebra.Etale R R'),
      ∃ P,
        ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
          ∃ e,
            ∃ (_ : IsIdempotentElem e),
              ∃ e₀,
                ∃ (_ : IsIdempotentElem e₀) (_ :
                  (Algebra.TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val) e₀ = e),
                  ∃ P',
                    ∃ (_ : P'.IsPrime) (_ : P'.LiesOver P),
                      Ideal.comap Algebra.TensorProduct.includeRight.toRingHom P' = q ∧
                        e ∉ P' ∧
                          Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (Algebra.ofId R R') ⋯) ∧
                            (∀ (P'' : Ideal (TensorProduct R R' ↥(integralClosure R S))),
                                P''.IsPrime →
                                  P''.LiesOver P →
                                    e₀ ∉ P'' →
                                      P'' =
                                        Ideal.comap
                                          (Algebra.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'

Defined in

Mathlib.RingTheory.Etale.QuasiFinite

Cited by

1 results in Mathlib

Foundations

Depth 168 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraAlgebra.FiniteTypeIdeal.IsPrimeIdeal.IsPrimeIdeal.LiesOverAlgebra.QuasiFiniteAt