AlgebraicGeometry.Scheme.Modules.zeroSchemeIdeal_eq_ofIdealTop_of_app_eq_smul
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_zeroSchemeIdeal_eq_ofIdealTop_of_app_eq_smul
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp] 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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.OppositeLean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.zeroSchemeIdeal_eq_ofIdealTop_of_app_eq_smul
{X : Scheme.{u}} (t : 𝟙_ X.Modules ⟶ 𝟙_ X.Modules) (r : Γ(X, ⊤))
(ht : t.app ⊤ (Scheme.Modules.toUnitSection ⊤ 1) = r • Scheme.Modules.toUnitSection ⊤ 1) :
Scheme.Modules.zeroSchemeIdeal t = Scheme.IdealSheafData.ofIdealTop (Ideal.span {r})