trace_eq_zero_of_finrank_eq_char_of_forall_isClosed_eq.lean

theorem trace_eq_zero_of_isLocalRing {k B : Type*} [Field k] [CommRing B] [Algebra k B]
  [Module.Finite k B]
    [IsLocalRing B] (h1 : Algebra.trace k B 1 = 0)
    (hres : Function.Surjective (algebraMap k (B ⧸ IsLocalRing.maximalIdeal B))) :
    Algebra.trace k B = 0

theorem mk_trace_eq {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] [Module.Free A B]
  [Module.Finite A B]
    (𝔪 : Ideal A) [𝔪.IsMaximal] (b : B) :
    Ideal.Quotient.mk 𝔪 (Algebra.trace A B b) = Algebra.trace (A ⧸ 𝔪) (B ⧸ 𝔪.map (algebraMap A B))
      (Ideal.Quotient.mk _ b)

theorem eq_zero_of_forall_mk_eq_zero {A : Type*} [CommRing A] [IsJacobsonRing A] [IsReduced A] (t :
  A)
    (h : ∀ 𝔪 : Ideal A, 𝔪.IsMaximal → Ideal.Quotient.mk 𝔪 t = 0) : t = 0

theorem isLocalRing_quotient_map {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] (𝔪 : Ideal
  A) [𝔪.IsMaximal]
    (huniq : ∀ N₁ N₂ : Ideal B, N₁.IsMaximal → N₂.IsMaximal →
      N₁.comap (algebraMap A B) = N₂.comap (algebraMap A B) → N₁ = N₂)
    [Nontrivial (B ⧸ 𝔪.map (algebraMap A B))] : IsLocalRing (B ⧸ 𝔪.map (algebraMap A B))

theorem isPullback_fromSpec :
    IsPullback (hU.preimage f).fromSpec (Spec.map (f.app U)) f hU.fromSpec

theorem maximal_eq_of_comap_eq [JacobsonSpace X]
    (hinj : ∀ x₁ x₂ : X, IsClosed ({x₁} : Set X) → IsClosed ({x₂} : Set X) → f.base x₁ = f.base x₂
      → x₁ = x₂)
    (N₁ N₂ : Ideal Γ(X, f ⁻¹ᵁ U)) (h₁ : N₁.IsMaximal) (h₂ : N₂.IsMaximal)
    (h : N₁.comap (f.app U).hom = N₂.comap (f.app U).hom) : N₁ = N₂

theorem finrank_eq [LocallyOfFinitePresentation f] (z : Spec Γ(Y, U)) :
    letI := (f.app U).hom.toAlgebra
    ∀ [Module.Free Γ(Y, U) Γ(X, f ⁻¹ᵁ U)] [Module.Finite Γ(Y, U) Γ(X, f ⁻¹ᵁ U)],
      Module.finrank Γ(Y, U) Γ(X, f ⁻¹ᵁ U) = f.finrank (hU.fromSpec.base z) := by
  intro _ _
  let _ := (f.app U).hom.toAlgebra
  have h1 := Scheme.Hom.finrank_of_isPullback _ _ _ _ (isPullback_fromSpec f U hU) z
  have h2 := Scheme.Hom.finrank_SpecMap_algebraMap Γ(Y, U) Γ(X, f ⁻¹ᵁ U) z
  rw [Module.rankAtStalk_eq_finrank_of_free] at h2
  have h3 : CommRingCat.ofHom (algebraMap Γ(Y, U) Γ(X, f ⁻¹ᵁ U)) = f.app U := CommRingCat.ofHom_hom
    _
  rw [h3, h1] at h2
  exact_mod_cast h2.symm

theorem _root_.AlgebraicGeometry.trace_eq_zero_of_finrank_eq_char_of_forall_isClosed_eq
    {κ : Type u} [Field κ] [IsAlgClosed κ] {p : ℕ} [Fact p.Prime] [CharP κ p]
    {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
    (fY : Y ⟶ Spec (CommRingCat.of κ)) [LocallyOfFiniteType fY]
    (f : X ⟶ Y) [IsFinite f] [Flat f] [LocallyOfFinitePresentation f] (hrk : ∀ y, f.finrank y = p)
    (hinj : ∀ x₁ x₂ : X, IsClosed ({x₁} : Set X) → IsClosed ({x₂} : Set X) → f.base x₁ = f.base x₂
      → x₁ = x₂)
    (U : Y.Opens) (hU : IsAffineOpen U) :
    letI := (f.app U).hom.toAlgebra
    ∀ [Module.Free Γ(Y, U) Γ(X, f ⁻¹ᵁ U)] [Module.Finite Γ(Y, U) Γ(X, f ⁻¹ᵁ U)],
      Algebra.trace Γ(Y, U) Γ(X, f ⁻¹ᵁ U) = 0 := by
  intro _ _
  classical
  let _ := (f.app U).hom.toAlgebra
  set A : Type u := ↑Γ(Y, U) with hA
  set B : Type u := ↑Γ(X, f ⁻¹ᵁ U) with hB
  rcases subsingleton_or_nontrivial A with hA0 | hA0
  · let _ : Subsingleton B := Module.subsingleton A B
    ext b; simp [Subsingleton.elim b 0]
  let ι₀ : κ →+* Γ(Spec (CommRingCat.of κ), ⊤) := (Scheme.ΓSpecIso (CommRingCat.of κ)).inv.hom
  have hι₀ : Function.Bijective ι₀ := ConcreteCategory.bijective_of_isIso (Scheme.ΓSpecIso
    (CommRingCat.of κ)).inv
  let φ : κ →+* A := (fY.appLE ⊤ U le_top).hom.comp ι₀
  let _ : Algebra κ A := φ.toAlgebra
  let _ : Algebra.FiniteType κ A := by
    have h1 : (fY.appLE ⊤ U le_top).hom.FiniteType := fY.finiteType_appLE (isAffineOpen_top _) hU
      le_top
    exact h1.comp (RingHom.FiniteType.of_surjective ι₀ hι₀.surjective)
  let _ : IsJacobsonRing A := isJacobsonRing_of_finiteType (A := κ) (B := A)
  let _ : JacobsonSpace X := LocallyOfFiniteType.jacobsonSpace (f ≫ fY)
  have hrank : Module.finrank A B = p := by
    obtain ⟨z⟩ := (inferInstance : Nonempty (Spec Γ(Y, U)))
    rw [finrank_eq f U hU z, hrk]
  ext b
  refine eq_zero_of_forall_mk_eq_zero _ fun 𝔪 h𝔪 => ?_
  let _ := h𝔪
  rw [mk_trace_eq 𝔪 b]
  let _ : Field (A ⧸ 𝔪) := Ideal.Quotient.field 𝔪
  rcases subsingleton_or_nontrivial (B ⧸ 𝔪.map (algebraMap A B)) with hB0 | hB0
  · rw [Subsingleton.elim (Ideal.Quotient.mk (𝔪.map (algebraMap A B)) b) 0, map_zero]
  let _ : Module.Finite (A ⧸ 𝔪) (B ⧸ 𝔪.map (algebraMap A B)) :=
    Module.Finite.of_restrictScalars_finite A _ _
  let _ : IsLocalRing (B ⧸ 𝔪.map (algebraMap A B)) :=
    isLocalRing_quotient_map 𝔪 (fun N₁ N₂ h₁ h₂ h => maximal_eq_of_comap_eq f U hU hinj N₁ N₂ h₁ h₂
      h)
  let _ : Module.Finite κ (A ⧸ 𝔪) := finite_of_finite_type_of_isJacobsonRing κ (A ⧸ 𝔪)
  have hbij : Function.Bijective (algebraMap κ (A ⧸ 𝔪)) :=
    IsAlgClosed.algebraMap_bijective_of_isIntegral
  let _ : IsAlgClosed (A ⧸ 𝔪) := IsAlgClosed.of_ringEquiv κ (A ⧸ 𝔪) (RingEquiv.ofBijective _ hbij)
  let _ : CharP (A ⧸ 𝔪) p := charP_of_injective_ringHom hbij.1 p
  have hres : Function.Surjective (algebraMap (A ⧸ 𝔪)
      ((B ⧸ 𝔪.map (algebraMap A B)) ⧸ IsLocalRing.maximalIdeal (B ⧸ 𝔪.map (algebraMap A B)))) := by
    let _ : Field ((B ⧸ 𝔪.map (algebraMap A B)) ⧸ IsLocalRing.maximalIdeal (B ⧸ 𝔪.map (algebraMap A
      B))) :=
      Ideal.Quotient.field _
    let _ : Module.Finite (A ⧸ 𝔪) ((B ⧸ 𝔪.map (algebraMap A B)) ⧸ IsLocalRing.maximalIdeal (B ⧸
      𝔪.map (algebraMap A B))) :=
      Module.Finite.of_surjective
        (Ideal.Quotient.mkₐ (A ⧸ 𝔪) (IsLocalRing.maximalIdeal (B ⧸ 𝔪.map (algebraMap A
          B)))).toLinearMap
        (Ideal.Quotient.mkₐ_surjective (A ⧸ 𝔪) (IsLocalRing.maximalIdeal (B ⧸ 𝔪.map (algebraMap A
          B))))
    exact (IsAlgClosed.algebraMap_bijective_of_isIntegral (k := A ⧸ 𝔪)).2
  have h1 : Algebra.trace (A ⧸ 𝔪) (B ⧸ 𝔪.map (algebraMap A B)) 1 = 0 := by
    rw [← map_one (Ideal.Quotient.mk (𝔪.map (algebraMap A B))), ← mk_trace_eq 𝔪 (1 : B),
      ← map_one (algebraMap A B), Algebra.trace_algebraMap, hrank, nsmul_eq_mul, mul_one,
        map_natCast,
      CharP.cast_eq_zero]
  rw [trace_eq_zero_of_isLocalRing h1 hres, LinearMap.zero_apply]