ModulesTensorPow.lean
Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesTensorPow
0 declarations indexed from sourceView source ↗
Module documentation
Tensor powers of scheme modules
Imports the maintained tensor power constructions for scheme modules.
Imported by58
- Nyll.AlgebraicCurves.Cohomology.Cech.Scheme_Modules_ProjPresentation_exists_forall_mul_pow_le_cechFinrank_zero_tensorPow
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_coeff_eq_rankAtStalk_mul_coeff_of_forall_eulerChar_twist_tensorPow_eq
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_degree_lt_of_forall_eulerChar_twist_tensorPow_eq_of_inter_iInter_support_zeroSchemeIdeal_eq_empty
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_eulerChar_twist_pushforwardUnit_succ_sub_eq
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_eulerChar_twist_pushforwardUnit_succ_sub_eq_of_not_subset_support_zeroSchemeIdeal
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_mvPolynomial_totalDegree_le_forall_eulerChar_tensor_eq
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_polynomial_forall_eulerChar_tensor_tensorPow_eq
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_polynomial_forall_eulerChar_twist_tensorPow_eq
- Nyll.AlgebraicCurves.Cohomology.Sheaves.Scheme_Modules_FiniteBySections_exists_polynomial_coeff_pos_forall_eulerChar_tensorPow_eq
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_exists_isClosed_irreducible_subset_fiber_of_not_quasiFiniteAt
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_subset_basicOpen_or_disjoint_of_isProper_of_isIrreducible
- Nyll.AlgebraicCurves.Geometry.Sheaves.All
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_FiniteBySections_tensorPow
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_tensorPowSection
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_tensorSections
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_isFrameOn
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_isFrameOn_app_of_disjoint_support_zeroSchemeIdeal
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_tensorPow
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ProjPresentation_exists_forall_le_forall_exists_notMem_support_zeroSchemeIdeal_tensor_tensorPow
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ProjPresentation_isFinite_toProj_of_finite_setOf_forall_pullbackSection_eq_zero_iff
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ProjPresentation_isFinite_toProj_of_forall_pullbackSection_eq_zero_iff
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ProjPresentation_subset_support_zeroSchemeIdeal_or_disjoint
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_away_finiteBySections_tensorPow_of_forall_geometricFibre
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_finiteBySections_tensorPow_of_forall_geometricFibre
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_forall_subsingleton_HSucc_tensorPow_of_isFinite_toProj
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_hom_tensorPow_three_support_zeroSchemeIdeal_eq
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_isFrameOn_tensorPow_three_of_forall_nonempty_pullback_tensor_iso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_isInvertible_hom_ne_zero_finite_setOf_stabilizer
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_isInvertible_normModule_pullback_pullback_iso_pullback
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isInvertible_of_forall_exists_isFrameOn
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isPrincipal_sub_sub_of_presentations_tensor
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_leftUnitor_hom_app_tensorSections
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_normModule_pullback_iso_tensorPow
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_pullback_tensorPow_iso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_tensorPow_mul_iso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_pullbackTensorObjIso_hom_app_pullbackLocalSection
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_pullbackTensorUnitObjIso_hom_app_pullbackLocalSection_unitSection
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_tensorPowSection_smul
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_whiskerLeft_app_tensorSections
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_whiskerRight_app_tensorSections
- Nyll.JacobianVarieties.Picard.AbelianSchemePropertyBundle_exists_isInvertible_coeff_pos_forall_eulerChar_tensorPow_eq
- Nyll.JacobianVarieties.Picard.AbelianSchemePropertyBundle_exists_isInvertible_finiteBySections
- Nyll.JacobianVarieties.Picard.Exists_finiteBySections_tensorPow_thetaBundle_of_isAlgClosed
- Nyll.JacobianVarieties.Picard.Exists_isFinite_proj_of_representsRelSubPic_algEquivZeroCut_of_finiteMapData
- Nyll.JacobianVarieties.Picard.IsAlgEquivZero_tensorPow
- Nyll.JacobianVarieties.Picard.RelativeGroupLaw_coeff_eq_endDegree_mul_coeff_of_forall_eulerChar_tensorPow_eq
- Nyll.JacobianVarieties.Picard.RelativeGroupLaw_coeff_eq_zero_of_not_isFinite_endKerStr_of_forall_eulerChar_tensorPow_eq
- Nyll.JacobianVarieties.Picard.RelativeGroupLaw_endDegree_nsmul_idPoint_eq_pow_of_natCast_ne_zero
- Nyll.JacobianVarieties.Picard.RelativeGroupLaw_exists_isInvertible_nonempty_pullback_inv_iso_coeff_pos_forall_eulerChar_tensorPow_eq
- Nyll.JacobianVarieties.Picard.RelativeGroupLaw_exists_polynomial_eval_eq_endDegree_zpow_mul_of_abelianSchemePropertyBundle
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_nonempty_poincare_pullbackAlong_pow_iso_tensorPow
- Nyll.JacobianVarieties.Picard.Scheme_Modules_nonempty_pullback_mul_mul_tensor_iso
- Nyll.JacobianVarieties.Picard.Scheme_Modules_nonempty_pullback_zpow_iso_tensorPow_of_symmetric
- Nyll.JacobianVarieties.Picard.fibrewiseAlgEquivZero_of_isAlgEquivZero_pullback_closedFibre_of_pullbackAlong_iso_tensorPow_poincare
This module has no indexed declarations. Its imports and full source are available here.