AlgebraicGeometry.Scheme.Modules.sheafificationAdjunction_unit_iotaMulti_eq_det_smul_of_eq_sum_smul
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedDeterminant
namespace AlgebraicGeometryLean source · full declaration
theorem Scheme.Modules.sheafificationAdjunction_unit_iotaMulti_eq_det_smul_of_eq_sum_smul
{X : Scheme.{u}} {M : X.Modules} {V : X.Opens} {d : ℕ} (f f' : Fin d → Γ(M, V))
(a : Matrix (Fin d) (Fin d) Γ(X, V)) (h : ∀ j, f' j = ∑ i, a i j • f i) :
(((PresheafOfModules.sheafificationAdjunction (𝟙 X.ringCatSheaf.obj)).unit.app
((Scheme.Modules.presheafExteriorPower X d).obj M.val)).app (op V)
(show ((Scheme.Modules.presheafExteriorPower X d).obj M.val).obj (op V) from
exteriorPower.ιMulti (M := Γ(M, V)) Γ(X, V) d f') :
Γ(Scheme.Modules.det d M, V)) =
a.det • (show Γ(Scheme.Modules.det d M, V) from
(((PresheafOfModules.sheafificationAdjunction (𝟙 X.ringCatSheaf.obj)).unit.app
((Scheme.Modules.presheafExteriorPower X d).obj M.val)).app (op V)
(show ((Scheme.Modules.presheafExteriorPower X d).obj M.val).obj (op V) from
exteriorPower.ιMulti (M := Γ(M, V)) Γ(X, V) d f))) := by
have key := Scheme.Modules.exteriorPower_map_app_unit_iotaMulti_eq_det_smul (𝟙 M) (U := V) f' f a
(fun j => by rw [h j]; rfl)
rw [CategoryTheory.Functor.map_id] at key
exact key