HenselianLocalRing_existsUnique_section_and_ker_eq_span_of_formallyUnramified_of_isLocalization.lean

theorem algebraMap_A [Algebra A S] [IsScalarTower A A[X] S] (a : A) :
    algebraMap A S a = algebraMap A[X] S (C a)

theorem mk_algebraMap_eq [Algebra A S] [IsScalarTower A A[X] S] (J₀ : Ideal S) (c : A)
    (hJ₀ : algebraMap A[X] S X - algebraMap A[X] S (C c) ∈ J₀) (p : A[X]) :
    (Ideal.Quotient.mk J₀ (algebraMap A[X] S p))
      = algebraMap A (S ⧸ J₀) (p.eval c)

theorem ker_fg (χ : S →+* A) (hC : ∀ a, χ (algebraMap A S a) = a) : (RingHom.ker χ).FG

theorem ker_eq_span [IsLocalRing A] [IsLocalRing S]
    [Algebra A S] [IsScalarTower A A[X] S] [Algebra.FormallyUnramified A[X] S]
    (χ : S →+* A) (hC : ∀ a, χ (algebraMap A[X] S (C a)) = a) (hfg : (RingHom.ker χ).FG) :
    RingHom.ker χ =
      Ideal.span {algebraMap A[X] S X - algebraMap A[X] S (C (χ (algebraMap A[X] S X)))}

theorem section_unique [IsLocalRing A] [IsLocalRing S]
    [Algebra A S] [IsScalarTower A A[X] S] [Algebra.FormallyUnramified A[X] S]
    (χ₁ χ₂ : S →+* A) (hC₁ : ∀ a, χ₁ (algebraMap A[X] S (C a)) = a)
    (hfg₁ : (RingHom.ker χ₁).FG)
    (hC₂ : ∀ a, χ₂ (algebraMap A[X] S (C a)) = a)
    (h : χ₁ (algebraMap A[X] S X) = χ₂ (algebraMap A[X] S X)) : χ₁ = χ₂

theorem exists_section [HenselianLocalRing A] [IsLocalRing S]
    [Algebra A S] [IsScalarTower A A[X] S] [Algebra.FormallySmooth A[X] S]
    {P : Type u} [CommRing P] [Algebra A P] [Algebra.FinitePresentation A P] (M : Submonoid P)
    [Algebra P S] [IsLocalization M S] [IsScalarTower A P S]
    (χ₀ : S →+* ResidueField A)
    (hχ₀C : ∀ a : A, χ₀ (algebraMap A[X] S (C a)) = IsLocalRing.residue A a)
    (hχ₀t : χ₀ (algebraMap A[X] S X) = 0)
    (c : A) (hc : IsLocalRing.residue A c = 0) :
    ∃ χ : S →+* A, (∀ a : A, χ (algebraMap A[X] S (C a)) = a) ∧
      (∀ f : S, IsLocalRing.residue A (χ f) = χ₀ f) ∧ χ (algebraMap A[X] S X) = c

theorem existsUnique_section_and_ker_eq_span_of_formallyUnramified_of_isLocalization
    {A : Type u} [CommRing A] [HenselianLocalRing A]
    {S : Type u} [CommRing S] [IsLocalRing S]
    (φ : Polynomial A →+* S) (hφs : φ.FormallySmooth) (hφu : φ.FormallyUnramified)
    (P : Type u) [CommRing P] [Algebra A P] [Algebra.FinitePresentation A P] (M : Submonoid P)
    [Algebra P S] [IsLocalization M S]
    (hPS : ∀ a : A, algebraMap P S (algebraMap A P a) = φ (Polynomial.C a))
    (χ₀ : S →+* ResidueField A) (_hχ₀ : RingHom.ker χ₀ = maximalIdeal S)
    (hχ₀C : ∀ a : A, χ₀ (φ (Polynomial.C a)) = IsLocalRing.residue A a) (hχ₀t : χ₀ (φ Polynomial.X)
      = 0) :
    (∀ c : A, IsLocalRing.residue A c = 0 →
      ∃! χ : S →+* A, (∀ a : A, χ (φ (Polynomial.C a)) = a) ∧
        (∀ f : S, IsLocalRing.residue A (χ f) = χ₀ f) ∧ χ (φ Polynomial.X) = c) ∧
    (∀ χ : S →+* A, (∀ a : A, χ (φ (Polynomial.C a)) = a) → (∀ f : S, IsLocalRing.residue A (χ f) =
      χ₀ f) →
      RingHom.ker χ = Ideal.span {φ Polynomial.X - φ (Polynomial.C (χ (φ Polynomial.X)))})