The inverse diamond lifts commute with the actual extension-field curve map

/-
Copyright (c) 2026 Vas and contributors. Released under Apache-2.0.
Design boundary: inverse diamond lifts commute with the actual curve map
from every characteristic-zero extension field to Q. Named downstream
consumer: geometric point line bundles of the rational Picard action.
-/
import Definitions.Def_MazurTransfer_Order13RationalGenericCurveLiftCompatibilityData

noncomputable section
namespace MazurTransfer.Order13GeometricInverseDiamondCurveNaturality
open CategoryTheory AlgebraicGeometry
open MazurTorsion.XOneThirteenProjectiveCurve
open GoodCharacteristicGeometryPublicProof.MazurTransfer.Order13GoodCharacteristicCurveModel
variable (K : Type) [Field K] [CharZero K]
local instance : Fact ((104 : K) ≠ 0) := ⟨by norm_num⟩
local instance : Fact ((104 : ℚ) ≠ 0) := ⟨by norm_num⟩

theorem existingDiamondCurve_inverse_baseChange :
    (Order13FieldDiamondGenericCurveOrder.genericDiamondCurveIso K).inv ≫
      Order13ActualCurveBaseChange.curveMap ℚ K =
    Order13ActualCurveBaseChange.curveMap ℚ K ≫
      Order13ActualDiamondGenericCurveOrder.genericDiamondCurveIso.inv := by
  let e : curveScheme K ≅ curveScheme K := Order13FieldDiamondGenericCurveOrder.genericDiamondCurveIso K
  let d : curveScheme ℚ ≅ curveScheme ℚ := Order13ActualDiamondGenericCurveOrder.genericDiamondCurveIso
  let b := Order13ActualCurveBaseChange.curveMap ℚ K
  change e.inv ≫ b = b ≫ d.inv
  apply (cancel_epi e.hom).mp
  have h : e.hom ≫ b = b ≫ d.hom :=
    Order13RationalGenericCurveLiftCompatibility.existingDiamondCurve_baseChange K
  rw [← Category.assoc, e.hom_inv_id, Category.id_comp, ← Category.assoc, h,
    Category.assoc, d.hom_inv_id, Category.comp_id]

end MazurTransfer.Order13GeometricInverseDiamondCurveNaturality
#print axioms MazurTransfer.Order13GeometricInverseDiamondCurveNaturality.existingDiamondCurve_inverse_baseChange