AlgebraicGeometry.Scheme.Modules.nonempty_normModule_unit_iso
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_normModule_unit_iso
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
CoherentBaseChange.TwoTermComplex.mk.injEq AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
AlgebraicGeometry.Scheme.Modules.tensorSections_zero_right
AlgebraicGeometry.Scheme.Modules.map_unitSection
AlgebraicGeometry.Scheme.Modules.tensorSectionsBilin_apply
AlgebraicGeometry.Scheme.Modules.tensorPowSection_zero
AlgebraicGeometry.Scheme.Modules.tensorSections_zero_left
AlgebraicGeometry.Scheme.Modules.tensorPow_zero AlgebraicGeometry.Scheme.Modules.tensorPow_succ
PresheafOfModules.pushforwardCongr_inv_app_app_apply
PresheafOfModules.pushforwardNatTrans_app_app_apply
PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometryLean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.nonempty_normModule_unit_iso {X Y : Scheme.{u}} (π
: X ⟶ Y) [IsFinite π] [Flat π] [LocallyOfFinitePresentation π]
(d : ℕ) (hd : ∀ y : Y, π.finrank y = d) :
Nonempty (Scheme.Modules.normModule π d (𝟙_ X.Modules) ≅ 𝟙_ Y.Modules)