IntegralSectionCartier.lean

theorem isEffectiveCartierAt_of_polynomial_chart
    (I : (ProjectiveLine ℤ).IdealSheafData)
    (j : Spec (CommRingCat.of ℤ[X]) ⟶ ProjectiveLine ℤ)
    [IsOpenImmersion j] (f : ℤ[X]) (hf : f ≠ 0)
    (htop :
      (I.comap j).ideal ⟨⊤, isAffineOpen_top (Spec (CommRingCat.of ℤ[X]))⟩ =
        (Ideal.span {f}).map (Scheme.ΓSpecIso (CommRingCat.of ℤ[X])).inv.hom)
    (q : Spec (CommRingCat.of ℤ[X])) :
    I.IsEffectiveCartierAt (j q)

theorem infinitySection_ker_isEffectiveCartier :
    (integralSection 1 0 1 0 (by decide)).ker.IsEffectiveCartier := by
  let I : (ProjectiveLine ℤ).IdealSheafData :=
    (integralSection 1 0 1 0 (by decide)).ker
  have hInf :
      (I.comap (infinityChartEmbedding ℤ)).ideal
          ⟨⊤, isAffineOpen_top (Spec (CommRingCat.of ℤ[X]))⟩ =
        (Ideal.span {(Polynomial.X : ℤ[X])}).map
          (Scheme.ΓSpecIso (CommRingCat.of ℤ[X])).inv.hom := by
    simpa only [I, infinitySectionIdeal, map_zero, map_one, one_mul,
      zero_sub, Ideal.span_singleton_neg] using
      integralSection_infinityChart_ideal_top 1 0 1 0 (by decide)
  have hj : infinityChartEmbedding ℤ ≫ (projectiveCoordinateSwap ℤ).inv =
      standardChartEmbedding ℤ := by
    rw [infinityChartEmbedding, Category.assoc,
      Iso.hom_inv_id, Category.comp_id]
  have hswapIdeal : I.comap (projectiveCoordinateSwap ℤ).inv =
      (integralSection 0 (-1) 0 (-1) (by decide)).ker :=
    integralSection_ker_comap_coordinateChange_inv
      0 1 0 1 1 0 1 0 0 (-1) (by decide) (by decide) (by decide)
  have hstdPull : I.comap (standardChartEmbedding ℤ) =
      (integralSection 0 (-1) 0 (-1) (by decide)).ker.comap
        (infinityChartEmbedding ℤ) := by
    rw [← hj, Scheme.IdealSheafData.comap_comp, hswapIdeal]
  have hStd :
      (I.comap (standardChartEmbedding ℤ)).ideal
          ⟨⊤, isAffineOpen_top (Spec (CommRingCat.of ℤ[X]))⟩ =
        (Ideal.span {(1 : ℤ[X])}).map
          (Scheme.ΓSpecIso (CommRingCat.of ℤ[X])).inv.hom := by
    rw [hstdPull]
    simpa only [infinitySectionIdeal, map_neg, map_one, map_zero,
      zero_mul, sub_zero, Ideal.span_singleton_neg] using
      integralSection_infinityChart_ideal_top 0 (-1) 0 (-1) (by decide)
  have hcover :
      (⨆ i : Fin 2, Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
        (MvPolynomial.X i)) = ⊤ :=
    Proj.iSup_basicOpen_eq_top (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
      (MvPolynomial.X : Fin 2 → MvPolynomial (Fin 2) ℤ)
      (ProjSpace.irrelevant_le_span_X ℤ 1)
  change I.IsEffectiveCartier
  intro x
  have hx : x ∈
      (⨆ i : Fin 2, Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
        (MvPolynomial.X i)) := by
    rw [hcover]
    trivial
  obtain ⟨i, hi⟩ := TopologicalSpace.Opens.mem_iSup.mp hx
  fin_cases i
  · have hmem : x ∈ (infinityChartEmbedding ℤ).opensRange := by
      rw [infinityChartEmbedding_opensRange]
      exact hi
    change x ∈ Set.range (infinityChartEmbedding ℤ) at hmem
    obtain ⟨q, rfl⟩ := hmem
    exact isEffectiveCartierAt_of_polynomial_chart I (infinityChartEmbedding ℤ)
      Polynomial.X Polynomial.X_ne_zero hInf q
  · have hmem : x ∈ (standardChartEmbedding ℤ).opensRange := by
      rw [standardChartEmbedding_opensRange, infinityComplement]
      exact hi
    change x ∈ Set.range (standardChartEmbedding ℤ) at hmem
    obtain ⟨q, rfl⟩ := hmem
    exact isEffectiveCartierAt_of_polynomial_chart I (standardChartEmbedding ℤ)
      1 one_ne_zero hStd q

theorem rationalSection_ker_isEffectiveCartier
    (a : Projectivization ℚ (ℚ × ℚ)) :
    (rationalSection a).ker.IsEffectiveCartier