GeometricStalkHenselianEmbedding.lean

theorem algebraic_of_genericFractionRing
    (R A : Type u) [CommRing R] [IsDomain R] [CommRing A]
    [Algebra R A]
    (hIntegral : Algebra.IsIntegral (FractionRing R) (FractionRing R ⊗[R] A))
    (hFraction :
      let : Algebra A (FractionRing R ⊗[R] A) := Algebra.TensorProduct.rightAlgebra
      IsFractionRing A (FractionRing R ⊗[R] A)) :
    Algebra.IsAlgebraic R A := by
  let K := FractionRing R
  let T := K ⊗[R] A
  let : Algebra A T := Algebra.TensorProduct.rightAlgebra
  have : IsFractionRing A T := hFraction
  have : Algebra.IsIntegral K T := hIntegral
  have : Algebra.IsAlgebraic R T :=
    (IsFractionRing.comap_isAlgebraic_iff (A := R) (K := K) (C := T)).mpr inferInstance
  exact Algebra.IsAlgebraic.of_injective
    (Algebra.TensorProduct.includeRight : A →ₐ[R] T) (IsFractionRing.injective A T)

theorem geometricStalk_isAlgebraic
    {R Ω : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R] [IsLocalRing R]
    [Field Ω] (φ : R →+* Ω) [IsLocalHom φ] :
    let : Algebra R (geometricStalk (Spec.map (CommRingCat.ofHom φ))) :=
      (geometricStalkStructureMap φ).toAlgebra
    Algebra.IsAlgebraic R (geometricStalk (Spec.map (CommRingCat.ofHom φ))) := by
  let G := geometricStalk (Spec.map (CommRingCat.ofHom φ))
  let : Algebra R G := (geometricStalkStructureMap φ).toAlgebra
  exact algebraic_of_genericFractionRing R G
    (geometricStalk_tensor_isIntegral φ (FractionRing R))
    (geometricStalk_genericTensor_isFractionRing φ)

theorem geometricStalkToHenselian_injective
    {R S : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R] [IsLocalRing R]
    [CommRing S] [HenselianLocalRing S]
    (f : R →+* S) [IsLocalHom f] (hf : Function.Injective f) :
    Function.Injective (geometricStalkToHenselian f)