germToFunctionField_trace_eq_traceFunAlong_germToFunctionField.lean

theorem _root_.AlgebraicGeometry.germToFunctionField_trace_eq_traceFunAlong_germToFunctionField
    {K : Type u} [Field K] {X Y : Scheme.{u}} (cX : X ⟶ Spec (.of K)) (cY : Y ⟶ Spec (.of K))
    [IsIntegral X] [IsIntegral Y] (π : Y ⟶ X) [IsAffineHom π] (_hπ : π ≫ cX = cY)
    (U : X.Opens) (hU : IsAffineOpen U) [Nonempty U] [Nonempty (π ⁻¹ᵁ U : Y.Opens)] :
    letI := (AlgebraicCurve.baseToFunctionField cX).toAlgebra
    letI := (AlgebraicCurve.baseToFunctionField cY).toAlgebra
    letI : Algebra Γ(X, U) Γ(Y, π ⁻¹ᵁ U) := (π.app U).hom.toAlgebra
    ∀ [Module.Free Γ(X, U) Γ(Y, π ⁻¹ᵁ U)] [Module.Finite Γ(X, U) Γ(Y, π ⁻¹ᵁ U)]
      (φ : X.functionField →ₐ[K] Y.functionField)
      (_hφπ : Y.fromSpecStalk (genericPoint Y) ≫ π =
        Spec.map (CommRingCat.ofHom φ.toRingHom) ≫ X.fromSpecStalk (genericPoint X))
      (g : Γ(Y, π ⁻¹ᵁ U)),
      (X.germToFunctionField U).hom (Algebra.trace Γ(X, U) Γ(Y, π ⁻¹ᵁ U) g) =
        AlgebraicCurve.traceFunAlong φ ((Y.germToFunctionField (π ⁻¹ᵁ U)).hom g) := by
  intro _ _ φ hφπ g
  let := (AlgebraicCurve.baseToFunctionField cX).toAlgebra
  let := (AlgebraicCurve.baseToFunctionField cY).toAlgebra
  let iAB : Algebra Γ(X, U) Γ(Y, π ⁻¹ᵁ U) := (π.app U).hom.toAlgebra
  let : Algebra X.functionField Y.functionField := AlgebraicCurve.algebraAlong φ
  have hUaff : IsAffineOpen (π ⁻¹ᵁ U) := hU.preimage π
  have : IsFractionRing Γ(X, U) X.functionField := functionField_isFractionRing_of_isAffineOpen X U
    hU
  have : IsFractionRing Γ(Y, π ⁻¹ᵁ U) Y.functionField :=
    functionField_isFractionRing_of_isAffineOpen Y _ hUaff
  have hnat : ∀ a : Γ(X, U), (Y.germToFunctionField (π ⁻¹ᵁ U)).hom (π.app U a) =
      φ ((X.germToFunctionField U).hom a) := fun a =>
    AlgebraicCurve.germToFunctionField_app_eq_of_fromSpecStalk_comp_eq π φ.toRingHom hφπ U a
  let : Algebra Γ(X, U) Y.functionField :=
    ((algebraMap Γ(Y, π ⁻¹ᵁ U) Y.functionField).comp (algebraMap Γ(X, U) Γ(Y, π ⁻¹ᵁ U))).toAlgebra
  have : IsScalarTower Γ(X, U) Γ(Y, π ⁻¹ᵁ U) Y.functionField :=
    IsScalarTower.of_algebraMap_eq (fun _ => rfl)
  have : IsScalarTower Γ(X, U) X.functionField Y.functionField :=
    IsScalarTower.of_algebraMap_eq (fun a => hnat a)
  have : FaithfulSMul Γ(X, U) Γ(Y, π ⁻¹ᵁ U) := by
    rw [faithfulSMul_iff_algebraMap_injective]
    intro a b hab
    have h := congrArg (fun t => (Y.germToFunctionField (π ⁻¹ᵁ U)).hom t) hab
    change (Y.germToFunctionField (π ⁻¹ᵁ U)).hom (π.app U a) =
      (Y.germToFunctionField (π ⁻¹ᵁ U)).hom (π.app U b) at h
    rw [hnat, hnat] at h
    exact X.germToFunctionField_injective U (φ.toRingHom.injective h)
  have : Algebra.IsIntegral Γ(X, U) Γ(Y, π ⁻¹ᵁ U) := Algebra.IsIntegral.of_finite _ _
  have : Algebra.IsAlgebraic Γ(X, U) Γ(Y, π ⁻¹ᵁ U) := Algebra.IsIntegral.isAlgebraic
  have key : Algebra.trace X.functionField Y.functionField (algebraMap Γ(Y, π ⁻¹ᵁ U)
    Y.functionField g) =
      algebraMap Γ(X, U) X.functionField (Algebra.trace Γ(X, U) Γ(Y, π ⁻¹ᵁ U) g) :=
    Algebra.trace_localization Γ(X, U) (nonZeroDivisors Γ(X, U)) g
  rw [AlgebraicCurve.traceFunAlong_apply]
  exact key.symm