AlgebraicGeometry.Scheme.Modules.exists_refinement_isFrameOn_normModule_map_eq_normFun_smul
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_refinement_isFrameOn_normModule_map_eq_normFun_smul
attribute [-instance]
AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
AlgebraicGeometry.Scheme.Modules.pullback_monoidal
AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
pullback_monoidal
isIso_δ
PresheafOfModules.pushforward_laxMonoidal
isIso_η
PresheafOfModules.free_monoidal
PresheafOfModules.restrictScalars_laxMonoidal
isIso_δ_gS
PresheafOfModules.pullback_oplaxMonoidal
instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
PresheafOfModules.pullback_monoidal'
SheafOfModules.isIso_ihomModelToIhom
attribute [-simp] PresheafOfModules.freeεIso_hom_app PresheafOfModules.freeμIso_hom_app
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
SheafOfModules.ihomSectionsEquivFamily_unit
AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply
SheafOfModules.unit_ihomSectionsEquivFamily AlgebraicGeometry.Scheme.Modules.familyOfHom_app
AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
open AlgebraicGeometry.Scheme.Modules.NormFLF in
Lean source · full declarationtheorem
_root_.AlgebraicGeometry.Scheme.Modules.exists_refinement_isFrameOn_normModule_map_eq_normFun_smul
{X Y : Scheme.{u}} (π : X ⟶ Y) [IsFinite π] [Flat π] [LocallyOfFinitePresentation π]
[Surjective π]
[IsIntegral X] [IsIntegral Y]
(d : ℕ) (hd : ∀ y : Y, π.finrank y = d)
(Nf : ∀ W : Y.Opens, Γ(X, π ⁻¹ᵁ W) → Γ(Y, W))
(h2 : ∀ (W W' : Y.Opens) (h : W' ≤ W) (a : Γ(X, π ⁻¹ᵁ W)),
Nf W' (X.presheaf.map (homOfLE (Scheme.Hom.preimage_mono π h)).op a) = Y.presheaf.map
(homOfLE h).op (Nf W a))
(h3 : ∀ (W : Y.Opens), IsAffineOpen W →
letI : Algebra Γ(Y, W) Γ(X, π ⁻¹ᵁ W) := (π.app W).hom.toAlgebra
∀ [Module.Free Γ(Y, W) Γ(X, π ⁻¹ᵁ W)] [Module.Finite Γ(Y, W) Γ(X, π ⁻¹ᵁ W)],
∀ a : Γ(X, π ⁻¹ᵁ W), Nf W a = Algebra.norm Γ(Y, W) a)
{ι : Type u} (U : ι → Y.Opens) (L : X.Modules) (s : ∀ i, Γ(L, π ⁻¹ᵁ U i))
(hs : ∀ i, Scheme.Modules.IsFrameOn (s i) (π ⁻¹ᵁ U i))
(u : ∀ i j, Γ(X, π ⁻¹ᵁ (U i ⊓ U j)))
(hu : ∀ i j, L.presheaf.map (homOfLE (Scheme.Hom.preimage_mono π inf_le_right)).op (s j) =
u i j • L.presheaf.map (homOfLE (Scheme.Hom.preimage_mono π inf_le_left)).op (s i)) :
∃ (κ : Type u) (T : κ → Y.Opens) (r : κ → ι), (⨆ k, T k) = ⨆ i, U i ∧ (∀ k, T k ≤ U (r k)) ∧
∃ Ω : ∀ k, Γ(Scheme.Modules.normModule π d L, T k),
(∀ k, Scheme.Modules.IsFrameOn (Ω k) (T k)) ∧
∀ (k l : κ) (hkl : T k ⊓ T l ≤ U (r k) ⊓ U (r l)),
(Scheme.Modules.normModule π d L).presheaf.map (homOfLE inf_le_right).op (Ω l) =
Y.presheaf.map (homOfLE hkl).op (Nf (U (r k) ⊓ U (r l)) (u (r k) (r l))) •
(Scheme.Modules.normModule π d L).presheaf.map (homOfLE inf_le_left).op (Ω k) := by
classical
have hLF : Scheme.Modules.IsLocallyFreeOfRank d ((Scheme.Modules.pushforward π).obj (𝟙_
X.Modules)) :=
Scheme.Modules.isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver π d hd
_
(fun y => ⟨⊤, trivial, ⟨Scheme.Modules.pullbackUnitIso _⟩⟩)
choose V hyV e he using fun y : Y => hLF.exists_basis y
let κ : Type u := Σ i : ι, ↥(U i)
let T : κ → Y.Opens := fun k => U k.1 ⊓ V k.2.1
let r : κ → ι := fun k => k.1
have hTU : ∀ k, T k ≤ U (r k) := fun k => inf_le_left
have hTV : ∀ k, T k ≤ V k.2.1 := fun k => inf_le_right
have hsup : (⨆ k, T k) = ⨆ i, U i := by
apply le_antisymm
· exact iSup_le fun k => (hTU k).trans (le_iSup U (r k))
· refine iSup_le fun i => fun y hy => ?_
exact Opens.mem_iSup.mpr ⟨⟨i, ⟨y, hy⟩⟩, ⟨hy, hyV y⟩⟩
let e' : ∀ k, Fin d → Γ((Scheme.Modules.pushforward π).obj (𝟙_ X.Modules), T k) := fun k i =>
((Scheme.Modules.pushforward π).obj (𝟙_ X.Modules)).presheaf.map (homOfLE (hTV k)).op (e k.2.1
i)
have he' : ∀ (k : κ) (W : Y.Opens) (hW : W ≤ T k),
∃ b : Module.Basis (Fin d) Γ(Y, W) Γ((Scheme.Modules.pushforward π).obj (𝟙_ X.Modules), W),
∀ i, b i = ((Scheme.Modules.pushforward π).obj (𝟙_ X.Modules)).presheaf.map (homOfLE hW).op
(e' k i) := by
intro k W hW
obtain ⟨b, hb⟩ := he k.2.1 W (hW.trans (hTV k))
refine ⟨b, fun i => ?_⟩
rw [hb i]
simp only [e', ← CategoryTheory.comp_apply, ← Functor.map_comp]
rfl
let s' : ∀ k, Γ(L, π ⁻¹ᵁ T k) := fun k => L.presheaf.map (homOfLE (Scheme.Hom.preimage_mono π
(hTU k))).op (s (r k))
have hs' : ∀ k, Scheme.Modules.IsFrameOn (s' k) (π ⁻¹ᵁ T k) := fun k =>
((hs (r k)).mono (Scheme.Hom.preimage_mono π (hTU k))).map _
let u' : ∀ k l, Γ(X, π ⁻¹ᵁ (T k ⊓ T l)) := fun k l => rX π (inf_le_inf (hTU k) (hTU l)) (u (r k)
(r l))
have hu' : ∀ k l, L.presheaf.map (homOfLE (Scheme.Hom.preimage_mono π inf_le_right)).op (s' l) =
u' k l • L.presheaf.map (homOfLE (Scheme.Hom.preimage_mono π inf_le_left)).op (s' k) := by
intro k l
have hkl : T k ⊓ T l ≤ U (r k) ⊓ U (r l) := inf_le_inf (hTU k) (hTU l)
have h := congrArg (L.presheaf.map (homOfLE (Scheme.Hom.preimage_mono π hkl)).op) (hu (r k) (r
l))
rw [Scheme.Modules.map_smul] at h
simp only [s', u', ← CategoryTheory.comp_apply, ← Functor.map_comp] at h ⊢
exact h
obtain ⟨Ω, hΩ, hΩtrans⟩ :=
Scheme.Modules.exists_isFrameOn_normModule_forall_map_eq_norm_smul_of_isFrameOn_preimage π d T
e' he' L s' hs' u' hu'
refine ⟨κ, T, r, hsup, hTU, Ω, hΩ, fun k l hkl => ?_⟩
rw [hΩtrans k l]
congr 1
let algO : Algebra Γ(Y, T k ⊓ T l) Γ(X, π ⁻¹ᵁ (T k ⊓ T l)) := (π.app (T k ⊓ T l)).hom.toAlgebra
obtain ⟨bO, hbO⟩ := he' k (T k ⊓ T l) inf_le_left
let bA : Module.Basis (Fin d) Γ(Y, T k ⊓ T l) Γ(X, π ⁻¹ᵁ (T k ⊓ T l)) := bO
let A := {W : Y.Opens // W ≤ T k ⊓ T l ∧ IsAffineOpen W}
have hcov : T k ⊓ T l ≤ ⨆ a : A, a.1 := by
intro y hy
obtain ⟨W', hW', hyW', hW'le⟩ := exists_isAffineOpen_mem_and_subset (X := Y) (x := y) (U := T k
⊓ T l) hy
exact Opens.mem_iSup.mpr ⟨⟨W', hW'le, hW'⟩, hyW'⟩
apply Y.sheaf.eq_of_locally_eq' (fun a : A => a.1) (T k ⊓ T l) (fun a => homOfLE a.2.1) hcov
rintro ⟨W', hW', hW'aff⟩
change rY hW' (Algebra.norm Γ(Y, T k ⊓ T l) (u' k l)) = rY hW' (rY hkl (Nf (U (r k) ⊓ U (r l)) (u
(r k) (r l))))
let algW : Algebra Γ(Y, W') Γ(X, π ⁻¹ᵁ W') := (π.app W').hom.toAlgebra
obtain ⟨bW, hbW⟩ := he' k W' (hW'.trans inf_le_left)
let bB : Module.Basis (Fin d) Γ(Y, W') Γ(X, π ⁻¹ᵁ W') := bW
have hb : ∀ i, bB i = rX π hW' (bA i) := by
intro i
have : bW i = ((Scheme.Modules.pushforward π).obj (𝟙_ X.Modules)).presheaf.map (homOfLE hW').op
(bO i) := by
rw [hbW i, hbO i]
simp only [e', ← CategoryTheory.comp_apply, ← Functor.map_comp]
rfl
exact this
rw [norm_map π hW' bA bB hb (u' k l)]
have : Module.Free Γ(Y, W') Γ(X, π ⁻¹ᵁ W') := Module.Free.of_basis bB
have : Module.Finite Γ(Y, W') Γ(X, π ⁻¹ᵁ W') := Module.Finite.of_basis bB
have eR : rY hW' (rY hkl (Nf (U (r k) ⊓ U (r l)) (u (r k) (r l)))) =
Nf W' (rX π (hW'.trans hkl) (u (r k) (r l))) := by
rw [rY_rY]
exact (h2 (U (r k) ⊓ U (r l)) W' (hW'.trans hkl) (u (r k) (r l))).symm
have eL : rX π hW' (u' k l) = rX π (hW'.trans hkl) (u (r k) (r l)) := by
simp only [u', rX_rX]
rw [eR, eL, h3 W' hW'aff]