Direct summand theorem and derived variant
Loading leaderboard data…
Problem statement
Notes: Unavailable.
Source: Unavailable.
Informal solution: Unavailable.
theorem declaration uses `sorry`derived_direct_summand [HasDerivedCategory (ModuleCat A)]
(X : Scheme) (f : X ⟶ Spec (.of A)) [IsProper f] (surj : Function.Surjective f)
[HasDerivedCategory (SheafOfModules X.ringCatSheaf)] :
let φ : A →+* Γ(X, ⊤) := ((ΓSpec.adjunction.homEquiv _ _).symm f).unop.hom
let : Algebra A Γ(X, ⊤) := φ.toAlgebra
∀ _ : EnoughInjectives (SheafOfModules X.ringCatSheaf), IsSplitMono <|
(DerivedCategory.Plus.singleFunctor _ 0).map
(ModuleCat.ofHom (Algebra.linearMap A Γ(X, ⊤))) ≫
(rightDerivedFunctorPlusUnit' (SheafOfModules.evaluation X.ringCatSheaf ⟨⊤⟩ ⋙
ModuleCat.restrictScalars φ) 0).app (SheafOfModules.unit X.ringCatSheaf) := A:Type u_1inst✝⁴:CommRing Ainst✝³:IsRegularRing Ainst✝²:HasDerivedCategory (ModuleCat A)X:Schemef:X ⟶ Spec (CommRingCat.of A)inst✝¹:IsProper fsurj:Function.Surjective ⇑finst✝:HasDerivedCategory (SheafOfModules X.ringCatSheaf)⊢ let φ := CommRingCat.Hom.hom ((ΓSpec.adjunction.homEquiv X (Opposite.op (CommRingCat.of A))).symm f).unop;
let this := φ.toAlgebra;
∀ (x : EnoughInjectives (SheafOfModules X.ringCatSheaf)),
IsSplitMono
((DerivedCategory.Plus.singleFunctor (ModuleCat A) 0).map (ModuleCat.ofHom (Algebra.linearMap A ↑Γ(X, ⊤))) ≫
(rightDerivedFunctorPlusUnit'
(SheafOfModules.evaluation X.ringCatSheaf (Opposite.op ⊤) ⋙ ModuleCat.restrictScalars φ) 0).app
(SheafOfModules.unit X.ringCatSheaf))
All goals completed! 🐙theorem declaration uses `sorry`direct_summand (B : Type*) [CommRing B] [Algebra A B]
[Module.Finite A B] [FaithfulSMul A B] :
∃ π : B →ₗ[A] A, π ∘ₗ Algebra.linearMap A B = .id := A:Type u_1inst✝⁵:CommRing Ainst✝⁴:IsRegularRing AB:Type u_2inst✝³:CommRing Binst✝²:Algebra A Binst✝¹:Module.Finite A Binst✝:FaithfulSMul A B⊢ ∃ π, π ∘ₗ Algebra.linearMap A B = LinearMap.id
All goals completed! 🐙