All.lean
Nyll.AlgebraicCurves.Cohomology.Sheaves.All
0 declarations indexed from sourceView source ↗
Imports83
- Nyll.AlgebraicCurves.Cohomology.Sheaves.BoundedCochainTensor
- Nyll.AlgebraicCurves.Cohomology.Sheaves.CoherentBaseChangeFamily
- Nyll.AlgebraicCurves.Cohomology.Sheaves.FppfCohomologyLES
- Nyll.AlgebraicCurves.Cohomology.Sheaves.FppfSiteCohomology
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheafEulerChar
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheafOfModules
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheafSectionsLinearRes
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheafTensor
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OrderedAffineCoverCochainPullback
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_AffHom_nonempty_H0_equiv_and_HSucc_equiv_of_bijective
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_AffSES_injective_inc_HSuccMap_of_forall_subsingleton_HSucc_of_surjective_proj_H0Map
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_Leray_exists_dTot_eq_single_biAug_unitPullback_sub_single_id
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_Leray_exists_levelwise_equiv_transpose_id
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_coeff_eq_rankAtStalk_mul_coeff_of_forall_eulerChar_twist_tensorPow_eq
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_d_unitPullback
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_d_zero_ofModules_eq_zero_iff_existsUnique
- 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_eq_zero_of_forall_res_basicOpen_eq_zero
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_eulerChar_eq_add_of_affSES
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_HSucc_equiv_unitPullback_id_of_isSeparated
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_affSES_tensor_of_flat
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_app_strip_eq_sum_of_box_zigzag_of_d_comap_slice_eq
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_box_zigzag_of_d_eq_zero_of_isAffineOpen
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_cochain_baseChange_equiv_of_locallyTrivial
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_d_eq_of_d_comap_section_eq_of_forall_preimage_chart
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_d_eq_of_d_comap_slice_eq_of_bijective_algebraMap
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_d_zero_eq_unitPullback_sub_unitPullback_of_d_one_eq_zero
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_eulerChar_twist_pushforwardUnit_succ_sub_eq
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_eulerChar_twist_pushforwardUnit_succ_sub_eq_monoidalV2
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_eulerChar_twist_pushforwardUnit_succ_sub_eq_of_not_subset_support_zeroSchemeIdeal
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_linearMap_apply_eq_unitPullback
- 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_tensor_tensorPow_eq_monoidalV2
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_polynomial_forall_eulerChar_twist_tensorPow_eq
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_polynomial_forall_eulerChar_twist_tensorPow_eq_monoidalV2
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_res_eq_sum_of_box_zigzag_of_exists_strip_eq_sum
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_res_eq_sum_of_d_comap_slice_eq_of_isAffineOpen
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_strip_eq_sum_of_forall_isAffineOpen_of_slice_of_bijective
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_strip_res_sub_eq_sum_of_box_zigzag_of_le
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_twoTermComplex_kerMapBaseChange_bijective_ofModules
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_flat_cochain_ofModules_of_locallyTrivial
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_forall_coherent_of_forall_integral
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_forall_of_forall_idealAnnihilates
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_forall_pushforward_of_isIntegral
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_isCoherent_ker
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_isCoherent_ofModules_of_locallyTrivial
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_isLocalizedModule_res_of_isQuasicoherent
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_isQuasicoherent_idealPow
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_isQuasicoherent_ker
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_isQuasicoherent_ofModules_of_locallyTrivial
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_map_app_unitPullback_eq_unitPullback_comp
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_nonempty_sections_top_equiv_H0_ofModules
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_od_oext
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_ores_oext
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_ores_ounitPullback_oext
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_projective_H0_and_bijective_kerBaseChangeHom_of_isReduced_of_finrank_eq
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_subsingleton_HSucc_and_eulerChar_eq_sum_range_of_card_le
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_subsingleton_HSucc_of_isQuasicoherent
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_unitPullback_comap_id_apply
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_unitPullback_unitPullback_sub_mem_of_d_eq_zero
- Nyll.AlgebraicCurves.Cohomology.Sheaves.ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback
- Nyll.AlgebraicCurves.Cohomology.Sheaves.ProjSpace_exists_polynomial_natDegree_le_forall_eulerChar_twist_stdCoverPullback_eq
- Nyll.AlgebraicCurves.Cohomology.Sheaves.ProjSpace_flat_cochain_twist_and_subsingleton_cochain_of_flat
- Nyll.AlgebraicCurves.Cohomology.Sheaves.RelEffCartierDiv_eulerChar_tensor_lineBundle_eq
- Nyll.AlgebraicCurves.Cohomology.Sheaves.RelEffCartierDiv_exists_I_eq_zeroSchemeIdeal_of_eulerChar_eq
- Nyll.AlgebraicCurves.Cohomology.Sheaves.RelEffCartierDiv_exists_I_eq_zeroSchemeIdeal_of_eulerChar_eq_of_smooth_fibre
- Nyll.AlgebraicCurves.Cohomology.Sheaves.Scheme_IdealSheafData_IsInvertible_eulerChar_sectionsOf_pullback_finsetProd_pow_invModule_tensor_and_module_tensor
- Nyll.AlgebraicCurves.Cohomology.Sheaves.Scheme_IdealSheafData_IsInvertible_eulerChar_sectionsOf_pullback_foldr_pow_invModule_tensor_pow_module_tensor_eq_add_sum
- Nyll.AlgebraicCurves.Cohomology.Sheaves.Scheme_IdealSheafData_IsInvertible_eulerChar_sectionsOf_pullback_pow_invModule_tensor_eq_add_mul
- Nyll.AlgebraicCurves.Cohomology.Sheaves.Scheme_IdealSheafData_IsInvertible_eulerChar_sectionsOf_pullback_pow_module_tensor_eq_sub_mul
- Nyll.AlgebraicCurves.Cohomology.Sheaves.Scheme_IdealSheafData_IsInvertible_eulerChar_sectionsOf_tensor_invModule_eq
- Nyll.AlgebraicCurves.Cohomology.Sheaves.Scheme_Modules_FiniteBySections_exists_polynomial_coeff_pos_forall_eulerChar_tensorPow_eq
- Nyll.AlgebraicCurves.Cohomology.Sheaves.Scheme_Modules_IsInvertible_eulerChar_sectionsOf_dual_eq
- Nyll.AlgebraicCurves.Cohomology.Sheaves.Scheme_Modules_IsInvertible_eulerChar_sectionsOf_tensor_eq_add_sub
- Nyll.AlgebraicCurves.Cohomology.Sheaves.Scheme_Modules_IsInvertible_nontrivial_H0_sectionsOf_of_le_eulerChar_sub
- Nyll.AlgebraicCurves.Cohomology.Sheaves.Scheme_Modules_IsInvertible_subsingleton_H1_sectionsOf_of_le_eulerChar_sub
- Nyll.AlgebraicCurves.Cohomology.Sheaves.Scheme_TwoAffineOpenCover_eulerChar_sectionsOf_invModule_pow_ker_tensor_module_prod_ker_eq
- Nyll.AlgebraicCurves.Cohomology.Sheaves.IsIso_baseChangeHom_pushforward_of_forall_fibre
Imported by1
This module has no indexed declarations. Its imports and full source are available here.