existsUnique_eq_appLE_add_eps_mul_appLE_of_isAffineOpen.lean

theorem _root_.AlgebraicGeometry.RelPicard.existsUnique_eq_appLE_add_eps_mul_appLE_of_isAffineOpen
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (A : Type u) [CommRing A]
      [Algebra R A]
    (U : (Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A)).Opens) (hU : IsAffineOpen U)
    (U' : (Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R (DualNumber A))).Opens)
    (hU' : RelPicard.baseChangeSnd c (RelPicard.LFP.stageHom R (IsScalarTower.toAlgHom R A
      (DualNumber A))) ⁻¹ᵁ U = U')
    (u : Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R (DualNumber A)), U')) :
    let _ : Algebra (DualNumber A)
        Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R (DualNumber A)), U') :=
      Scheme.TwoAffineOpenCover.algebraOfHom
      (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R (DualNumber A))) U'
    ∃! ab : Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A), U) ×
        Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A), U),
      u = ((RelPicard.baseChangeSnd c
              (RelPicard.LFP.stageHom R (IsScalarTower.toAlgHom R A (DualNumber A)))).appLE U U'
                hU'.ge).hom ab.1
          + algebraMap (DualNumber A) _ DualNumber.eps *
            ((RelPicard.baseChangeSnd c
              (RelPicard.LFP.stageHom R (IsScalarTower.toAlgHom R A (DualNumber A)))).appLE U U'
                hU'.ge).hom ab.2 := by
  intro iU'
  let iU : Algebra A Γ(Limits.pullback c (specMap R A), U) :=
    Scheme.TwoAffineOpenCover.algebraOfHom (Limits.pullback.snd c (specMap R A)) U
  obtain ⟨e, he⟩ :=
    RelPicard.exists_algEquiv_sections_stage_baseChange_of_isAffineOpen c A (DualNumber A) U hU U'
      hU'
  set σ := (RelPicard.baseChangeSnd c
    (RelPicard.LFP.stageHom R (IsScalarTower.toAlgHom R A (DualNumber A)))).appLE U U' hU'.ge with
      hσdef
  have hε : ∀ b : Γ(Limits.pullback c (specMap R A), U),
      (DualNumber.eps ⊗ₜ[A] b : DualNumber A ⊗[A] Γ(Limits.pullback c (specMap R A), U)) =
        algebraMap (DualNumber A) (DualNumber A ⊗[A] Γ(Limits.pullback c (specMap R A), U))
          DualNumber.eps *
          ((1 : DualNumber A) ⊗ₜ[A] b) := fun b => by
    rw [Algebra.TensorProduct.algebraMap_apply, Algebra.TensorProduct.tmul_mul_tmul, mul_one,
      one_mul]
    rfl
  have hdec : ∀ a b : Γ(Limits.pullback c (specMap R A), U),
      e ((1 : DualNumber A) ⊗ₜ[A] a + DualNumber.eps ⊗ₜ[A] b) =
        σ.hom a + algebraMap (DualNumber A) _ DualNumber.eps * σ.hom b := fun a b => by
    rw [map_add, he, hε, map_mul, AlgEquiv.commutes, he]
  have hsplit : ∀ t : DualNumber A ⊗[A] Γ(Limits.pullback c (specMap R A), U),
      ∃ a b, t = (1 : DualNumber A) ⊗ₜ[A] a + DualNumber.eps ⊗ₜ[A] b := by
    intro t
    induction t using TensorProduct.inductionOn with
    | tmul d s =>
      refine ⟨(TrivSqZeroExt.fst d) • s, (TrivSqZeroExt.snd d) • s, ?_⟩
      rw [tmul_smul, tmul_smul, smul_tmul', smul_tmul', ← add_tmul]
      congr 1
      refine TrivSqZeroExt.ext ?_ ?_ <;>
        simp only [TrivSqZeroExt.fst_add, TrivSqZeroExt.snd_add,
          TrivSqZeroExt.fst_smul, TrivSqZeroExt.snd_smul, TrivSqZeroExt.fst_one,
          TrivSqZeroExt.snd_one, DualNumber.fst_eps, DualNumber.snd_eps,
          smul_eq_mul, mul_one, mul_zero, add_zero, zero_add]
    | add x y hx hy =>
      obtain ⟨a, b, rfl⟩ := hx
      obtain ⟨a', b', rfl⟩ := hy
      exact ⟨a + a', b + b', by rw [tmul_add, tmul_add]; abel⟩
  let fstL : DualNumber A →ₗ[A] A :=
    { toFun := TrivSqZeroExt.fst, map_add' := fun x y => TrivSqZeroExt.fst_add x y,
      map_smul' := fun r x => TrivSqZeroExt.fst_smul r x }
  let sndL : DualNumber A →ₗ[A] A :=
    { toFun := TrivSqZeroExt.snd, map_add' := fun x y => TrivSqZeroExt.snd_add x y,
      map_smul' := fun r x => TrivSqZeroExt.snd_smul r x }
  let pa : DualNumber A ⊗[A] Γ(Limits.pullback c (specMap R A), U) →ₗ[A] Γ(Limits.pullback c
    (specMap R A), U) :=
    (TensorProduct.lid A _).toLinearMap ∘ₗ TensorProduct.map fstL LinearMap.id
  let pb : DualNumber A ⊗[A] Γ(Limits.pullback c (specMap R A), U) →ₗ[A] Γ(Limits.pullback c
    (specMap R A), U) :=
    (TensorProduct.lid A _).toLinearMap ∘ₗ TensorProduct.map sndL LinearMap.id
  have hpa : ∀ a b : Γ(Limits.pullback c (specMap R A), U),
      pa ((1 : DualNumber A) ⊗ₜ[A] a + DualNumber.eps ⊗ₜ[A] b) = a := fun a b => by
    rw [map_add]
    change TrivSqZeroExt.fst (1 : DualNumber A) • a +
      TrivSqZeroExt.fst (DualNumber.eps : DualNumber A) • b = a
    rw [TrivSqZeroExt.fst_one, DualNumber.fst_eps, one_smul, zero_smul, add_zero]
  have hpb : ∀ a b : Γ(Limits.pullback c (specMap R A), U),
      pb ((1 : DualNumber A) ⊗ₜ[A] a + DualNumber.eps ⊗ₜ[A] b) = b := fun a b => by
    rw [map_add]
    change TrivSqZeroExt.snd (1 : DualNumber A) • a +
      TrivSqZeroExt.snd (DualNumber.eps : DualNumber A) • b = b
    rw [TrivSqZeroExt.snd_one, DualNumber.snd_eps, zero_smul, one_smul, zero_add]
  obtain ⟨a, b, hab⟩ := hsplit (e.symm u)
  have hu : u = σ.hom a + algebraMap (DualNumber A) _ DualNumber.eps * σ.hom b := by
    rw [← hdec, ← hab, AlgEquiv.apply_symm_apply]
  refine ⟨(a, b), hu, ?_⟩
  rintro ⟨a', b'⟩ h'
  have key : (1 : DualNumber A) ⊗ₜ[A] a' + DualNumber.eps ⊗ₜ[A] b' = (1 : DualNumber A) ⊗ₜ[A] a +
    DualNumber.eps ⊗ₜ[A] b := by
    apply e.injective
    rw [hdec, hdec, ← hu]
    exact h'.symm
  have ha := congrArg pa key
  have hb := congrArg pb key
  rw [hpa, hpa] at ha
  rw [hpb, hpb] at hb
  rw [ha, hb]