GeometricStalkTensorLocal.lean

theorem etale_hom_exists_base_preimage
    {T E L : Type u} [CommRing T] [CommRing E] [CommRing L]
    [Algebra T E] [Algebra T L] [HenselianLocalRing T] [IsLocalRing L]
    [IsSepClosed (IsLocalRing.ResidueField T)] [Algebra.Etale T E]
    [IsLocalHom (algebraMap T L)] (g : E →ₐ[T] L) (e : E) :
    ∃ t : T, algebraMap T L t = g e

theorem geometricStalk_hom_exists_strictHenselian_preimage
    {R Ω T L : Type u} [CommRing R] [Field Ω] [CommRing T] [CommRing L]
    [Algebra R T] [Algebra R L] [Algebra T L] [IsScalarTower R T L]
    [HenselianLocalRing T] [IsLocalRing L]
    [IsSepClosed (IsLocalRing.ResidueField T)]
    [IsLocalHom (algebraMap T L)] (φ : R →+* Ω)
    (g : geometricStalk (Spec.map (CommRingCat.ofHom φ)) →+* L)
    (hg : g.comp (geometricStalkStructureMap φ) = algebraMap R L)
    (a : geometricStalk (Spec.map (CommRingCat.ofHom φ))) :
    ∃ t : T, algebraMap T L t = g a

theorem geometricStalk_tensor_localizationAtPrime_bijective
    {R Ω T : Type u} [CommRing R] [Field Ω] [CommRing T] [Algebra R T]
    [HenselianLocalRing T] [IsSepClosed (IsLocalRing.ResidueField T)]
    (φ : R →+* Ω) :
    let H := geometricStalk (Spec.map (CommRingCat.ofHom φ))
    let : Algebra R H := (geometricStalkStructureMap φ).toAlgebra
    ∀ (q : Ideal (T ⊗[R] H)) [q.IsPrime]
      [q.LiesOver (IsLocalRing.maximalIdeal T)],
      Function.Bijective (algebraMap T (Localization.AtPrime q)) := by
  intro H hH q hq hqover
  let B := T ⊗[R] H
  let L := Localization.AtPrime q
  have : Module.Flat R H := geometricStalkStructureMap_flat φ
  have : IsLocalHom (algebraMap T L) :=
    isLocalHom_algebraMap_localizationAtPrime_of_liesOver_maximalIdeal q
  have : Module.FaithfullyFlat T L := Module.FaithfullyFlat.of_flat_of_isLocalHom
  refine ⟨FaithfulSMul.algebraMap_injective T L, ?_⟩
  let g : H →+* L := (algebraMap B L).comp
    (Algebra.TensorProduct.includeRight : H →ₐ[R] B).toRingHom
  have hg : g.comp (geometricStalkStructureMap φ) = algebraMap R L := by
    apply RingHom.ext
    intro r
    have hcoeff : (Algebra.TensorProduct.includeRight : H →ₐ[R] B)
        (algebraMap R H r) = algebraMap R B r :=
      (Algebra.TensorProduct.includeRight : H →ₐ[R] B).commutes r
    exact (congrArg (algebraMap B L) hcoeff).trans
      (IsScalarTower.algebraMap_apply R B L r).symm
  have hpreimage (b : B) : ∃ t : T, algebraMap T L t = algebraMap B L b := by
    induction b using TensorProduct.inductionOn with
    | tmul t a =>
      obtain ⟨r, hr⟩ := geometricStalk_hom_exists_strictHenselian_preimage
        (R := R) (Ω := Ω) (T := T) (L := L) φ g hg a
      refine ⟨t * r, ?_⟩
      calc
        algebraMap T L (t * r) = algebraMap T L t * g a := by rw [map_mul, hr]
        _ = algebraMap B L ((t ⊗ₜ[R] (1 : H)) * (1 ⊗ₜ[R] a)) := by
          rw [map_mul]
          change algebraMap T L t * g a =
            algebraMap B L (algebraMap T B t) * g a
          rw [← IsScalarTower.algebraMap_apply]
        _ = algebraMap B L (t ⊗ₜ[R] a) := by
          rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]
    | add b c hb hc =>
      obtain ⟨t, ht⟩ := hb
      obtain ⟨r, hr⟩ := hc
      exact ⟨t + r, by rw [map_add, ht, hr, map_add]⟩
  intro x
  obtain ⟨b, s, rfl⟩ := IsLocalization.exists_mk'_eq q.primeCompl x
  obtain ⟨t, ht⟩ := hpreimage b
  obtain ⟨d, hd⟩ := hpreimage s
  have hdunit : IsUnit d := IsLocalHom.map_nonunit d
    (hd.symm ▸ IsLocalization.map_units L s)
  obtain ⟨dunit, hdunit⟩ := hdunit
  refine ⟨t * ↑(dunit⁻¹), ?_⟩
  apply IsLocalization.eq_mk'_iff_mul_eq.mpr
  rw [← hd, ← hdunit, ← map_mul, mul_assoc, Units.inv_mul, mul_one, ht]