HenselianFullness.lean

theorem exists_idempotent_ker_of_surjective
    {R : Type u} {A : Type v} {B : Type w}
    [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    [Algebra.Etale R A] [Algebra.Etale R B]
    (f : A →ₐ[R] B) (hf : Function.Surjective f) :
    ∃ e : A, IsIdempotentElem e ∧ RingHom.ker f.toRingHom = Ideal.span {e}

theorem exists_lift_section_of_finite_henselian_base
    {R : Type u} {B : Type v} {C : Type w}
    [CommRing R] [CommRing B] [CommRing C]
    [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
    [Module.Finite R B] [Module.Finite B C] [Algebra.Etale B C]
    (I : Ideal R) [HenselianRing R I]
    (σ : C →ₐ[B] B ⧸ I.map (algebraMap R B)) :
    ∃ g : C →ₐ[B] B,
      (Ideal.Quotient.mkₐ B (I.map (algebraMap R B))).comp g = σ

theorem quotientBaseChange_surjective_of_henselian
    {R : Type u} {A : Type v} {B : Type w}
    [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    [Module.Finite R A] [Algebra.Etale R A]
    [Module.Finite R B] [Algebra.Etale R B]
    (I : Ideal R) [HenselianRing R I] :
    Function.Surjective (fun f : A →ₐ[R] B ↦ f.quotientBaseChange I) := by
  intro φ
  let J : Ideal B := I.map (algebraMap R B)
  let φR : A →ₐ[R] B ⧸ J :=
    (φ.restrictScalars R).comp (Ideal.Quotient.mkₐ R (I.map (algebraMap R A)))
  let σ : B ⊗[R] A →ₐ[B] B ⧸ J :=
    Algebra.TensorProduct.lift (Algebra.ofId B (B ⧸ J)) φR (fun _ _ ↦ .all _ _)
  obtain ⟨g, hg⟩ := exists_lift_section_of_finite_henselian_base I σ
  let f : A →ₐ[R] B := (g.restrictScalars R).comp Algebra.TensorProduct.includeRight
  refine ⟨f, AlgHom.ext fun x ↦ ?_⟩
  obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective x
  change Ideal.Quotient.mk J (g ((1 : B) ⊗ₜ[R] a)) =
    φ (Ideal.Quotient.mk (I.map (algebraMap R A)) a)
  have h := AlgHom.congr_fun hg ((1 : B) ⊗ₜ[R] a)
  change Ideal.Quotient.mk J (g ((1 : B) ⊗ₜ[R] a)) = σ ((1 : B) ⊗ₜ[R] a) at h
  simpa only [σ, Algebra.TensorProduct.lift_tmul, map_one, one_mul, φR,
    AlgHom.coe_comp, Function.comp_apply, AlgHom.restrictScalars_apply,
    Ideal.Quotient.mkₐ_eq_mk] using h

theorem baseChange_surjective_of_henselian
    {R : Type u} {A : Type v} {B : Type w}
    [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    [Module.Finite R A] [Algebra.Etale R A]
    [Module.Finite R B] [Algebra.Etale R B]
    (I : Ideal R) [HenselianRing R I] :
    Function.Surjective (fun f : A →ₐ[R] B ↦
      Algebra.TensorProduct.map (.id (R ⧸ I) (R ⧸ I)) f) := by
  intro ψ
  let eA := Algebra.TensorProduct.quotIdealMapEquivQuotTensor A I
  let eB := Algebra.TensorProduct.quotIdealMapEquivQuotTensor B I
  let φ := eB.symm.toAlgHom.comp (ψ.comp eA.toAlgHom)
  obtain ⟨f, hf⟩ := quotientBaseChange_surjective_of_henselian I φ
  refine ⟨f, AlgHom.ext fun t ↦ ?_⟩
  obtain ⟨x, rfl⟩ := eA.surjective t
  have h := AlgHom.congr_fun (f.quotientBaseChange_tensorProduct I) x
  change f.quotientBaseChange I = φ at hf
  rw [hf] at h
  change eB (φ x) =
    (Algebra.TensorProduct.map (.id (R ⧸ I) (R ⧸ I)) f) (eA x) at h
  change (Algebra.TensorProduct.map (.id (R ⧸ I) (R ⧸ I)) f) (eA x) =
    ψ (eA x)
  calc
    _ = eB (φ x) := h.symm
    _ = eB (eB.symm (ψ (eA x))) := by
      simp only [φ, AlgHom.comp_apply, AlgEquiv.toAlgHom_apply]
    _ = ψ (eA x) := eB.apply_symm_apply _

theorem baseChange_full_of_henselian
    {R : Type u} [CommRing R] (I : Ideal R) [HenselianRing R I] :
    (baseChange R (R ⧸ I) : CommAlgCat.FiniteEtale.{v} R ⥤
      CommAlgCat.FiniteEtale.{max u v} (R ⧸ I)).Full where
  map_surjective {A B} φ := by
    obtain ⟨f, hf⟩ := Algebra.FiniteEtale.baseChange_surjective_of_henselian I φ.hom.hom
    refine ⟨FiniteEtale.ofHom f, ?_⟩
    apply ObjectProperty.hom_ext
    apply CommAlgCat.Hom.ext
    exact hf