Nyll.SchemeTheory.Etale.PurelyInseparableFiniteFactor

theorem

purelyInseparable_of_bijective

AlgebraicGeometry.purelyInseparable_of_bijective

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace AlgebraicGeometry

Lean source · statement

theorem purelyInseparable_of_bijective
    {K L : Type*} [Field K] [Field L] (f : K →+* L)
    (hf : Function.Bijective f) : f.IsPurelyInseparable

theorem

exists_purelyInseparable_etale_finite_factor

L44 ↗

AlgebraicGeometry.exists_purelyInseparable_etale_finite_factor

Documentation

A selected purely inseparable residue extension stays purely inseparable in the actual finite open factor supplied by the quasi-finite local structure theorem. The conclusion records the actual finite map and its singleton fiber.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace AlgebraicGeometry

Lean source · statement

theorem exists_purelyInseparable_etale_finite_factor
    {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    [Algebra.FiniteType R A] (p : Ideal R) [p.IsPrime]
    (q : Ideal A) [q.IsPrime] [q.LiesOver p] [Algebra.QuasiFiniteAt R q]
    (hκ : (Ideal.ResidueField.map p q (algebraMap R A)
      (q.over_def p)).IsPurelyInseparable) :
    ∃ (R' : Type u) (_ : CommRing R') (_ : Algebra R R') (_ : Algebra.Etale R R')
      (P : Ideal R') (_ : P.IsPrime) (_ : P.LiesOver p)
      (e : R' ⊗[R] A) (_ : IsIdempotentElem e),
      Module.Finite R' (Localization.Away e) ∧
      IsFinite (Spec.map (CommRingCat.ofHom (algebraMap R' (Localization.Away e)))) ∧
      IsOpenImmersion (Spec.map (CommRingCat.ofHom
        (algebraMap (R' ⊗[R] A) (Localization.Away e)))) ∧
      ∃ z : Spec (CommRingCat.of (Localization.Away e)),
        Spec.map (CommRingCat.ofHom (algebraMap R' (Localization.Away e))) z =
          ⟨P, inferInstance⟩ ∧
        (Spec.map (CommRingCat.ofHom (algebraMap (R' ⊗[R] A) (Localization.Away e))) ≫
          Spec.map (CommRingCat.ofHom
            (Algebra.TensorProduct.includeRight : A →ₐ[R] R' ⊗[R] A).toRingHom)) z =
          (⟨q, inferInstance⟩ : Spec (CommRingCat.of A)) ∧
        (∀ z' : Spec (CommRingCat.of (Localization.Away e)),
          Spec.map (CommRingCat.ofHom (algebraMap R' (Localization.Away e))) z' =
            ⟨P, inferInstance⟩ → z' = z) ∧
        ((Spec.map (CommRingCat.ofHom (algebraMap R' (Localization.Away e)))).residueFieldMap
          z).hom.IsPurelyInseparable

PurelyInseparableFiniteFactor.lean

Module documentation

The residue extension of an actual finite local factor

purelyInseparable_of_bijective

exists_purelyInseparable_etale_finite_factor

Module documentation

The residue extension of an actual finite local factor

Declarations

purelyInseparable_of_bijective

exists_purelyInseparable_etale_finite_factor