AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartGluedLinesSectionsEquiv.TwoChartCech.GluedLinesTriv.forward
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartGluedLinesSectionsEquiv
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open scoped Polynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesTriv
section Forward
variable {k : Type u} [Field k] {s : ℕ} (a b : Fin s → kˣ) (hb : Function.Injective b) (lam : Fin s
→ kˣ)
(n m : ℤ)
include hb
Lean source · full declarationtheorem forward
(g₀ : letI := (gluedLinesSections k a b lam n m).M0_moduleA
(gluedLinesSections k a b lam n m).M0 ≃ₗ[(gluedLinesCover k a b).A0] (gluedLinesCover k a
b).structureSheaf.M0)
(g₁ : letI := (gluedLinesSections k a b lam n m).M1_moduleA
(gluedLinesSections k a b lam n m).M1 ≃ₗ[(gluedLinesCover k a b).A1] (gluedLinesCover k a
b).structureSheaf.M1)
(g₀₁ : letI := (gluedLinesSections k a b lam n m).M01_moduleA
(gluedLinesSections k a b lam n m).M01 ≃ₗ[(gluedLinesCover k a b).A01] (gluedLinesCover k a
b).structureSheaf.M01)
(h₀ : ∀ t, g₀₁ ((gluedLinesSections k a b lam n m).r0 t) = (gluedLinesCover k a
b).structureSheaf.r0 (g₀ t))
(h₁ : ∀ t, g₀₁ ((gluedLinesSections k a b lam n m).r1 t) = (gluedLinesCover k a
b).structureSheaf.r1 (g₁ t)) :
n = 0 ∧ m = 0 ∧ ∀ i j, lam i = lam j := by
classical
let := (gluedLinesSections k a b lam n m).M0_moduleA
let := (gluedLinesSections k a b lam n m).M1_moduleA
let := (gluedLinesSections k a b lam n m).M01_moduleA
set w : ↥(gluedLinesM01 k a b lam) := g₀₁.symm 1 with hw
have hmul : ∀ f : ↥(gluedLinesM01 k a b lam),
(f : k[T;T⁻¹] × k[T;T⁻¹]) = ((g₀₁ f : ↥(gluedLinesOverlap k a b)) : k[T;T⁻¹] × k[T;T⁻¹]) * w
:= by
intro f
have hf : f = (g₀₁ f) • w := by
let r : ↥(gluedLinesOverlap k a b) := g₀₁ f
have hr : r • (1 : ↥(gluedLinesOverlap k a b)) = r :=
(smul_eq_mul r 1).trans (mul_one r)
have hs : g₀₁.symm r = r • g₀₁.symm 1 :=
(congrArg (fun x : ↥(gluedLinesOverlap k a b) => g₀₁.symm x) hr.symm).trans
(g₀₁.symm.map_smul r 1)
exact (g₀₁.symm_apply_apply f).symm.trans hs
exact congrArg Subtype.val hf
set t₀ : ↥(gluedLinesM0 k a b lam) := g₀.symm 1 with ht₀
set t₁ : ↥(gluedLinesM1 k a b lam n m) := g₁.symm 1 with ht₁
have hwt₀ : (w : k[T;T⁻¹] × k[T;T⁻¹]) = (t₀ : k[T;T⁻¹] × k[T;T⁻¹]) := by
have h := h₀ t₀
rw [ht₀, LinearEquiv.apply_symm_apply] at h
have h1 : (gluedLinesCover k a b).structureSheaf.r0 (1 : (gluedLinesCover k a b).A0) = 1 := by
change (gluedLinesCover k a b).ρ0 1 = 1; exact map_one _
rw [h1] at h
have h2 : (gluedLinesSections k a b lam n m).r0 (g₀.symm 1) = w := by
rw [hw, ← h, LinearEquiv.symm_apply_apply]
rw [← ht₀] at h2
exact (congrArg Subtype.val h2).symm
have hwt₁ : (w : k[T;T⁻¹] × k[T;T⁻¹]) = (t₁ : k[T;T⁻¹] × k[T;T⁻¹]) := by
have h := h₁ t₁
rw [ht₁, LinearEquiv.apply_symm_apply] at h
have h1 : (gluedLinesCover k a b).structureSheaf.r1 (1 : (gluedLinesCover k a b).A1) = 1 := by
change (1 : (gluedLinesCover k a b).A01) * (gluedLinesCover k a b).ρ1 1 = 1
rw [map_one, one_mul]
rw [h1] at h
have h2 : (gluedLinesSections k a b lam n m).r1 (g₁.symm 1) = w := by
rw [hw, ← h, LinearEquiv.symm_apply_apply]
rw [← ht₁] at h2
exact (congrArg Subtype.val h2).symm
have hmul₀ : ∀ t : ↥(gluedLinesM0 k a b lam),
(t : k[T;T⁻¹] × k[T;T⁻¹]) = ((g₀ t : (gluedLinesCover k a b).A0) : k[T;T⁻¹] × k[T;T⁻¹]) * w
:= by
intro t
have h := hmul ((gluedLinesSections k a b lam n m).r0 t)
rw [h₀ t] at h
exact h
have hmul₁ : ∀ t : ↥(gluedLinesM1 k a b lam n m),
(t : k[T;T⁻¹] × k[T;T⁻¹]) = ((g₁ t : (gluedLinesCover k a b).A1) : k[T;T⁻¹] × k[T;T⁻¹]) * w
:= by
intro t
have h := hmul ((gluedLinesSections k a b lam n m).r1 t)
rw [h₁ t] at h
have h' : (((gluedLinesCover k a b).structureSheaf.r1 (g₁ t) : (gluedLinesCover k a b).A01) :
k[T;T⁻¹] × k[T;T⁻¹]) = ((g₁ t : (gluedLinesCover k a b).A1) : k[T;T⁻¹] × k[T;T⁻¹]) := by
change (((1 : (gluedLinesCover k a b).A01) * (gluedLinesCover k a b).ρ1 (g₁ t) :
(gluedLinesCover k a b).A01) :
k[T;T⁻¹] × k[T;T⁻¹]) = _
rw [one_mul]; rfl
rw [h'] at h
exact h
have hwpoly : (w : k[T;T⁻¹] × k[T;T⁻¹]).1 ∈ polyPart k ∧ (w : k[T;T⁻¹] × k[T;T⁻¹]).2 ∈ polyPart k
:= by
rw [hwt₀]; exact Subalgebra.mem_prod.mp t₀.2.2
have hwM1 : (w : k[T;T⁻¹] × k[T;T⁻¹]).1 * T (-n) ∈ invPolyPart k ∧
(w : k[T;T⁻¹] × k[T;T⁻¹]).2 * T (-m) ∈ invPolyPart k := by
rw [hwt₁]; exact ⟨t₁.2.2.1, t₁.2.2.2⟩
have hwcond : GluedCond a b lam (w : k[T;T⁻¹] × k[T;T⁻¹]) := w.2
obtain ⟨Q, hQb, hQ0⟩ := exists_poly_eval_eq_and_eval_zero b hb (fun i => (((lam i)⁻¹ : kˣ) : k)) 1
have hf₁mem : ((1 : k[T;T⁻¹]), Polynomial.toLaurent Q) ∈ gluedLinesM0 k a b lam := by
refine ⟨fun i => ?_, Subalgebra.mem_prod.mpr ⟨Subalgebra.one_mem _, toLaurent_mem_polyPart Q⟩⟩
change levalUnit k (a i) 1 = lam i * levalUnit k (b i) (Polynomial.toLaurent Q)
rw [map_one, levalUnit_toLaurent, hQb, Units.mul_inv]
have hψeq := hmul₀ ⟨_, hf₁mem⟩
set ψ := ((g₀ ⟨_, hf₁mem⟩ : (gluedLinesCover k a b).A0) : k[T;T⁻¹] × k[T;T⁻¹]) with hψ
have hψ₁ : (1 : k[T;T⁻¹]) = ψ.1 * (w : k[T;T⁻¹] × k[T;T⁻¹]).1 := congrArg Prod.fst hψeq
have hQeq : Polynomial.toLaurent Q = ψ.2 * (w : k[T;T⁻¹] × k[T;T⁻¹]).2 := congrArg Prod.snd hψeq
have hψpoly : ψ.1 ∈ polyPart k ∧ ψ.2 ∈ polyPart k := Subalgebra.mem_prod.mp (g₀ ⟨_, hf₁mem⟩).2.2
have hw1unit : IsUnit (w : k[T;T⁻¹] × k[T;T⁻¹]).1 :=
IsUnit.of_mul_eq_one ψ.1 (by rw [mul_comm]; exact hψ₁.symm)
obtain ⟨c₁, d₁, hc₁, hw1⟩ := LaurentAux.exists_eq_C_mul_T_of_isUnit hw1unit
have hd₁ : 0 ≤ d₁ := hwpoly.1 d₁
(by rw [hw1, support_C_mul_T hc₁]; exact Finset.mem_singleton_self _)
have hCC : ∀ {c : k} (hc : c ≠ 0) (d : ℤ),
LaurentPolynomial.C c * T d * (LaurentPolynomial.C c⁻¹ * T (-d)) = 1 := by
intro c hc d
rw [mul_mul_mul_comm, ← map_mul, mul_inv_cancel₀ hc, map_one, one_mul, ← T_add, add_neg_cancel,
T_zero]
have hψ1eq : ψ.1 = LaurentPolynomial.C c₁⁻¹ * T (-d₁) := by
have h : ψ.1 * (LaurentPolynomial.C c₁ * T d₁) = 1 := by rw [← hw1]; exact hψ₁.symm
calc ψ.1 = ψ.1 * (LaurentPolynomial.C c₁ * T d₁) * (LaurentPolynomial.C c₁⁻¹ * T (-d₁)) := by
rw [mul_assoc, hCC hc₁, mul_one]
_ = LaurentPolynomial.C c₁⁻¹ * T (-d₁) := by rw [h, one_mul]
have hd₁' : d₁ ≤ 0 := by
have := hψpoly.1 (-d₁)
(by rw [hψ1eq, support_C_mul_T (inv_ne_zero hc₁)]; exact Finset.mem_singleton_self _)
omega
have hd₁0 : d₁ = 0 := le_antisymm hd₁' hd₁
rw [hd₁0, T_zero, mul_one] at hw1
set Pb : k[X] := ∏ i, (Polynomial.X - Polynomial.C (b i : k)) with hPb
have hPb0 : Pb ≠ 0 := by
rw [hPb]; exact Finset.prod_ne_zero_iff.mpr (fun i _ => Polynomial.X_sub_C_ne_zero _)
have hf₂mem : ((0 : k[T;T⁻¹]), Polynomial.toLaurent Pb) ∈ gluedLinesM01 k a b lam := by
intro i
change levalUnit k (a i) 0 = lam i * levalUnit k (b i) (Polynomial.toLaurent Pb)
rw [map_zero, levalUnit_toLaurent, hPb, Polynomial.eval_prod,
Finset.prod_eq_zero (Finset.mem_univ i) (by simp), mul_zero]
have hφeq := hmul ⟨_, hf₂mem⟩
set φ := ((g₀₁ ⟨_, hf₂mem⟩ : (gluedLinesCover k a b).A01) : k[T;T⁻¹] × k[T;T⁻¹]) with hφ
have hφ1 : (0 : k[T;T⁻¹]) = φ.1 * (w : k[T;T⁻¹] × k[T;T⁻¹]).1 := congrArg Prod.fst hφeq
have hφ2 : Polynomial.toLaurent Pb = φ.2 * (w : k[T;T⁻¹] × k[T;T⁻¹]).2 := congrArg Prod.snd hφeq
have hC₁ne : LaurentPolynomial.C c₁ ≠ 0 := fun h => hc₁ (by
have := congrArg (levalUnit k 1) h; rwa [levalUnit_C, map_zero] at this)
have hφ1z : φ.1 = 0 := by
rw [hw1] at hφ1
rcases mul_eq_zero.mp hφ1.symm with h | h
· exact h
· exact absurd h hC₁ne
have hφroots : ∀ i, levalUnit k (b i) φ.2 = 0 := by
intro i
have h := (g₀₁ ⟨_, hf₂mem⟩).2 i
change levalUnit k (a i) φ.1 = levalUnit k (b i) φ.2 at h
rw [← h, hφ1z, map_zero]
obtain ⟨N, Φ, hΦ⟩ := LaurentPolynomial.exists_T_pow φ.2
have hΦroots : ∀ i, Φ.IsRoot (b i : k) := by
intro i
have h := congrArg (levalUnit k (b i)) hΦ
rw [levalUnit_toLaurent, map_mul, hφroots i, zero_mul] at h
exact h
have hdvd : Pb ∣ Φ := by
rw [hPb]
apply Finset.prod_dvd_of_coprime
· intro i _ j _ hij
exact Polynomial.pairwise_coprime_X_sub_C (fun i j h => hb (Units.ext h)) hij
· intro i _; exact Polynomial.dvd_iff_isRoot.mpr (hΦroots i)
obtain ⟨Θ, hΘ⟩ := hdvd
have hw2unit : IsUnit (w : k[T;T⁻¹] × k[T;T⁻¹]).2 := by
have h1 : Polynomial.toLaurent Pb * T N =
Polynomial.toLaurent Pb * (Polynomial.toLaurent Θ * (w : k[T;T⁻¹] × k[T;T⁻¹]).2) := by
calc Polynomial.toLaurent Pb * T N = φ.2 * (w : k[T;T⁻¹] × k[T;T⁻¹]).2 * T N := by rw [← hφ2]
_ = (φ.2 * T N) * (w : k[T;T⁻¹] × k[T;T⁻¹]).2 := by ring
_ = Polynomial.toLaurent Φ * (w : k[T;T⁻¹] × k[T;T⁻¹]).2 := by rw [hΦ]
_ = Polynomial.toLaurent Pb * (Polynomial.toLaurent Θ * (w : k[T;T⁻¹] × k[T;T⁻¹]).2) := by
rw [hΘ, map_mul, mul_assoc]
have h2 : T (N : ℤ) = Polynomial.toLaurent Θ * (w : k[T;T⁻¹] × k[T;T⁻¹]).2 :=
mul_left_cancel₀ (Polynomial.toLaurent_ne_zero.mpr hPb0) h1
refine IsUnit.of_mul_eq_one (Polynomial.toLaurent Θ * T (-(N : ℤ))) ?_
calc (w : k[T;T⁻¹] × k[T;T⁻¹]).2 * (Polynomial.toLaurent Θ * T (-(N : ℤ)))
= (Polynomial.toLaurent Θ * (w : k[T;T⁻¹] × k[T;T⁻¹]).2) * T (-(N : ℤ)) := by ring
_ = T N * T (-(N : ℤ)) := by rw [← h2]
_ = 1 := by rw [← T_add, add_neg_cancel, T_zero]
obtain ⟨c₂, d₂, hc₂, hw2⟩ := LaurentAux.exists_eq_C_mul_T_of_isUnit hw2unit
have hd₂ : 0 ≤ d₂ := hwpoly.2 d₂
(by rw [hw2, support_C_mul_T hc₂]; exact Finset.mem_singleton_self _)
have hd₂' : d₂ ≤ 0 := by
have h0 : (0 : ℤ) ∈ (Polynomial.toLaurent Q : k[T;T⁻¹]).coeff.support :=
zero_mem_support_toLaurent
(by rw [Polynomial.coeff_zero_eq_eval_zero, hQ0]; exact one_ne_zero)
rw [hQeq, hw2, ← mul_assoc, mem_support_mul_T_iff, zero_sub] at h0
have hmem : ψ.2 * LaurentPolynomial.C c₂ ∈ polyPart k := Subalgebra.mul_mem _ hψpoly.2
(C_mem_polyPart c₂)
have := hmem (-d₂) h0
omega
have hd₂0 : d₂ = 0 := le_antisymm hd₂' hd₂
rw [hd₂0, T_zero, mul_one] at hw2
refine ⟨?_, ?_, ?_⟩
· apply le_antisymm
· obtain ⟨Q', hQ'⟩ := exists_poly_eval_inv_eq b hb (fun i => (((lam i)⁻¹ * a i ^ n * (b i ^
m)⁻¹ : kˣ) : k))
have hmem₃ : (T n, T m * invert (Polynomial.toLaurent Q')) ∈ gluedLinesM1 k a b lam n m := by
refine ⟨fun i => ?_, ?_, ?_⟩
· change levalUnit k (a i) (T n) = lam i * levalUnit k (b i) (T m * invert
(Polynomial.toLaurent Q'))
rw [levalUnit_T, map_mul, levalUnit_T, levalUnit_invert, levalUnit_toLaurent, hQ']
have hu : lam i * (b i ^ m * ((lam i)⁻¹ * a i ^ n * (b i ^ m)⁻¹)) = a i ^ n := by
rw [show (lam i)⁻¹ * a i ^ n * (b i ^ m)⁻¹ = (b i ^ m)⁻¹ * ((lam i)⁻¹ * a i ^ n) from
by rw [mul_comm]]
rw [← mul_assoc (b i ^ m), mul_inv_cancel, one_mul, ← mul_assoc, mul_inv_cancel,
one_mul]
exact_mod_cast hu.symm
· change T n * T (-n) ∈ invPolyPart k
rw [← T_add, add_neg_cancel, T_zero]; exact Subalgebra.one_mem _
· change T m * invert (Polynomial.toLaurent Q') * T (-m) ∈ invPolyPart k
rw [mul_comm (T m), mul_assoc, ← T_add, add_neg_cancel, T_zero, mul_one]
exact invert_mem_invPolyPart (toLaurent_mem_polyPart Q')
have h := congrArg Prod.fst (hmul₁ ⟨_, hmem₃⟩)
change T n = ((g₁ ⟨_, hmem₃⟩ : (gluedLinesCover k a b).A1) : k[T;T⁻¹] × k[T;T⁻¹]).1 *
(w : k[T;T⁻¹] × k[T;T⁻¹]).1 at h
rw [hw1] at h
have hψ₃ : ((g₁ ⟨_, hmem₃⟩ : (gluedLinesCover k a b).A1) : k[T;T⁻¹] × k[T;T⁻¹]).1 =
LaurentPolynomial.C c₁⁻¹ * T n := by
calc _ = ((g₁ ⟨_, hmem₃⟩ : (gluedLinesCover k a b).A1) : k[T;T⁻¹] × k[T;T⁻¹]).1 *
LaurentPolynomial.C c₁ * LaurentPolynomial.C c₁⁻¹ := by
rw [mul_assoc, ← map_mul, mul_inv_cancel₀ hc₁, map_one, mul_one]
_ = LaurentPolynomial.C c₁⁻¹ * T n := by rw [← h, mul_comm]
have hinv : ((g₁ ⟨_, hmem₃⟩ : (gluedLinesCover k a b).A1) : k[T;T⁻¹] × k[T;T⁻¹]).1 ∈
invPolyPart k :=
(Subalgebra.mem_prod.mp (g₁ ⟨_, hmem₃⟩).2.2).1
exact hinv n
(by rw [hψ₃, support_C_mul_T (inv_ne_zero hc₁)]; exact Finset.mem_singleton_self _)
· have h := hwM1.1
rw [hw1] at h
have := h (-n) (by rw [support_C_mul_T hc₁]; exact Finset.mem_singleton_self _)
omega
· apply le_antisymm
· set Pb' : k[X] := ∏ i, (Polynomial.X - Polynomial.C (((b i)⁻¹ : kˣ) : k)) with hPb'
have hmem₄ : ((0 : k[T;T⁻¹]), T m * invert (Polynomial.toLaurent Pb')) ∈ gluedLinesM1 k a b
lam n m := by
refine ⟨fun i => ?_, ?_, ?_⟩
· change levalUnit k (a i) 0 = lam i * levalUnit k (b i) (T m * invert
(Polynomial.toLaurent Pb'))
rw [map_zero, map_mul, levalUnit_invert, levalUnit_toLaurent, hPb', Polynomial.eval_prod,
Finset.prod_eq_zero (Finset.mem_univ i) (by simp), mul_zero, mul_zero]
· change (0 : k[T;T⁻¹]) * T (-n) ∈ invPolyPart k
rw [zero_mul]; exact Subalgebra.zero_mem _
· change T m * invert (Polynomial.toLaurent Pb') * T (-m) ∈ invPolyPart k
rw [mul_comm (T m), mul_assoc, ← T_add, add_neg_cancel, T_zero, mul_one]
exact invert_mem_invPolyPart (toLaurent_mem_polyPart Pb')
have h := congrArg Prod.snd (hmul₁ ⟨_, hmem₄⟩)
change T m * invert (Polynomial.toLaurent Pb') =
((g₁ ⟨_, hmem₄⟩ : (gluedLinesCover k a b).A1) : k[T;T⁻¹] × k[T;T⁻¹]).2 * (w : k[T;T⁻¹] ×
k[T;T⁻¹]).2 at h
rw [hw2] at h
have hψ₄ : ((g₁ ⟨_, hmem₄⟩ : (gluedLinesCover k a b).A1) : k[T;T⁻¹] × k[T;T⁻¹]).2 =
c₂⁻¹ • (T m * invert (Polynomial.toLaurent Pb')) := by
rw [← C_mul_eq_smul]
calc _ = ((g₁ ⟨_, hmem₄⟩ : (gluedLinesCover k a b).A1) : k[T;T⁻¹] × k[T;T⁻¹]).2 *
LaurentPolynomial.C c₂ * LaurentPolynomial.C c₂⁻¹ := by
rw [mul_assoc, ← map_mul, mul_inv_cancel₀ hc₂, map_one, mul_one]
_ = LaurentPolynomial.C c₂⁻¹ * (T m * invert (Polynomial.toLaurent Pb')) :=
by rw [← h, mul_comm]
have hinv : ((g₁ ⟨_, hmem₄⟩ : (gluedLinesCover k a b).A1) : k[T;T⁻¹] × k[T;T⁻¹]).2 ∈
invPolyPart k :=
(Subalgebra.mem_prod.mp (g₁ ⟨_, hmem₄⟩).2.2).2
refine hinv m ?_
rw [hψ₄, support_smul_of_ne_zero (inv_ne_zero hc₂), mul_comm (T m), mem_support_mul_T_iff,
sub_self,
LaurentAux.mem_support_invert_iff, neg_zero]
apply zero_mem_support_toLaurent
rw [Polynomial.coeff_zero_eq_eval_zero, hPb', Polynomial.eval_prod]
exact Finset.prod_ne_zero_iff.mpr (fun i _ => by simp)
· have h := hwM1.2
rw [hw2] at h
have := h (-m) (by rw [support_C_mul_T hc₂]; exact Finset.mem_singleton_self _)
omega
· intro i j
have hi := hwcond i
have hj := hwcond j
change levalUnit k (a i) (w : k[T;T⁻¹] × k[T;T⁻¹]).1 = lam i * levalUnit k (b i) (w : k[T;T⁻¹]
× k[T;T⁻¹]).2 at hi
change levalUnit k (a j) (w : k[T;T⁻¹] × k[T;T⁻¹]).1 = lam j * levalUnit k (b j) (w : k[T;T⁻¹]
× k[T;T⁻¹]).2 at hj
rw [hw1, hw2, levalUnit_C, levalUnit_C] at hi hj
apply Units.ext
exact mul_right_cancel₀ hc₂ (hi.symm.trans hj)