AffineResidueField.lean

theorem residueFieldIso_inv_residueFieldMap
    {R S : CommRingCat.{u}} (f : R ⟶ S) (x : Spec S) :
    letI : x.asIdeal.IsPrime := x.isPrime
    letI : (Spec.map f x).asIdeal.IsPrime := (Spec.map f x).isPrime
    (residueFieldIso R (Spec.map f x)).inv ≫
        (Spec.map f).residueFieldMap x ≫ (residueFieldIso S x).hom =
      CommRingCat.ofHom (Ideal.ResidueField.map
        (Spec.map f x).asIdeal x.asIdeal f.hom rfl) := by
  let : x.asIdeal.IsPrime := x.isPrime
  let : (Spec.map f x).asIdeal.IsPrime := (Spec.map f x).isPrime
  have heval :
      CommRingCat.ofHom (algebraMap R (Spec.map f x).asIdeal.ResidueField) ≫
          (residueFieldIso R (Spec.map f x)).inv ≫
          (Spec.map f).residueFieldMap x ≫ (residueFieldIso S x).hom =
        f ≫ CommRingCat.ofHom (algebraMap S x.asIdeal.ResidueField) := by
    rw [algebraMap_residueFieldIso_inv_assoc]
    change (Scheme.ΓSpecIso R).inv ≫ (Spec R).Γevaluation (Spec.map f x) ≫
        (Spec.map f).residueFieldMap x ≫ (residueFieldIso S x).hom = _
    rw [Scheme.Γevaluation_naturality_assoc, ← Scheme.ΓSpecIso_inv_naturality_assoc]
    change f ≫ (Scheme.ΓSpecIso S).inv ≫ (Spec S).presheaf.germ ⊤ x trivial ≫
        (Spec S).residue x ≫ (residueFieldIso S x).hom = _
    rw [← algebraMap_residueFieldIso_inv_assoc, Iso.inv_hom_id, Category.comp_id]
  apply CommRingCat.hom_ext
  apply Ideal.ResidueField.ringHom_ext
  apply RingHom.ext
  intro r
  have h := congrArg (fun k : R ⟶ CommRingCat.of x.asIdeal.ResidueField ↦ k r) heval
  change (residueFieldIso S x).hom
      ((Spec.map f).residueFieldMap x
        ((residueFieldIso R (Spec.map f x)).inv
          (algebraMap R (Spec.map f x).asIdeal.ResidueField r))) =
    Ideal.ResidueField.map (Spec.map f x).asIdeal x.asIdeal f.hom rfl
      (algebraMap R (Spec.map f x).asIdeal.ResidueField r)
  exact h.trans
    (Ideal.ResidueField.map_algebraMap (Spec.map f x).asIdeal x.asIdeal f.hom rfl r).symm

theorem ringEquiv_isPurelyInseparable
    {K L : Type u} [Field K] [Field L] (e : K ≃+* L) :
    e.toRingHom.IsPurelyInseparable

theorem residueFieldMap_isPurelyInseparable_iff
    {R S : CommRingCat.{u}} (f : R ⟶ S) (x : Spec S) :
    letI : x.asIdeal.IsPrime := x.isPrime
    letI : (Spec.map f x).asIdeal.IsPrime := (Spec.map f x).isPrime
    ((Spec.map f).residueFieldMap x).hom.IsPurelyInseparable ↔
      (Ideal.ResidueField.map
        (Spec.map f x).asIdeal x.asIdeal f.hom rfl).IsPurelyInseparable := by
  let : x.asIdeal.IsPrime := x.isPrime
  let : (Spec.map f x).asIdeal.IsPrime := (Spec.map f x).isPrime
  let eR := residueFieldIso R (Spec.map f x)
  let eS := residueFieldIso S x
  have hR : eR.hom.hom.IsPurelyInseparable :=
    ringEquiv_isPurelyInseparable eR.commRingCatIsoToRingEquiv
  have hRinv : eR.inv.hom.IsPurelyInseparable :=
    ringEquiv_isPurelyInseparable eR.symm.commRingCatIsoToRingEquiv
  have hS : eS.hom.hom.IsPurelyInseparable :=
    ringEquiv_isPurelyInseparable eS.commRingCatIsoToRingEquiv
  have hSinv : eS.inv.hom.IsPurelyInseparable :=
    ringEquiv_isPurelyInseparable eS.symm.commRingCatIsoToRingEquiv
  constructor
  · intro h
    have hcomp := hRinv.comp (h.comp hS)
    change (eR.inv ≫ (Spec.map f).residueFieldMap x ≫ eS.hom).hom.IsPurelyInseparable
      at hcomp
    rw [residueFieldIso_inv_residueFieldMap] at hcomp
    exact hcomp
  · intro h
    have hcomp := hR.comp (h.comp hSinv)
    change (eR.hom ≫ CommRingCat.ofHom (Ideal.ResidueField.map
        (Spec.map f x).asIdeal x.asIdeal f.hom rfl) ≫ eS.inv).hom.IsPurelyInseparable
      at hcomp
    rw [← residueFieldIso_inv_residueFieldMap] at hcomp
    change (eR.hom ≫ (eR.inv ≫ (Spec.map f).residueFieldMap x ≫ eS.hom) ≫
      eS.inv).hom.IsPurelyInseparable at hcomp
    simp only [Category.assoc, Iso.hom_inv_id_assoc, Iso.hom_inv_id,
      Category.comp_id] at hcomp
    exact hcomp