All.lean
Nyll.AlgebraicCurves.Cohomology.Cech.All
0 declarations indexed from sourceView source ↗
Imports84
- Nyll.AlgebraicCurves.Cohomology.Cech.BiCech
- Nyll.AlgebraicCurves.Cohomology.Cech.DivisorSections
- Nyll.AlgebraicCurves.Cohomology.Cech.Maps
- Nyll.AlgebraicCurves.Cohomology.Cech.OModulePresheafCechPushforward
- Nyll.AlgebraicCurves.Cohomology.Cech.OrderedAffineCoverCechCup
- Nyll.AlgebraicCurves.Cohomology.Cech.OrderedAffineCoverCechOrdered
- Nyll.AlgebraicCurves.Cohomology.Cech.CoherentBaseChange_FibreH0Family_isClosed_setOf_le_h0
- Nyll.AlgebraicCurves.Cohomology.Cech.CoherentBaseChange_TwoTermComplex_exists_nonempty_H0_linearEquiv_annihilator_of_fibreH0_le_one
- Nyll.AlgebraicCurves.Cohomology.Cech.CoherentBaseChange_TwoTermComplex_natCast_finrank_ker_baseChange_sub_natCast_finrank_quotient_range_eq_chi
- Nyll.AlgebraicCurves.Cohomology.Cech.CoherentBaseChange_TwoTermComplex_one_tmul_ne_zero_of_forall_nonempty_H0_linearEquiv
- Nyll.AlgebraicCurves.Cohomology.Cech.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
- Nyll.AlgebraicCurves.Cohomology.Cech.Cover_LaurentChart_residue_eq_kaehlerResidueTerm
- Nyll.AlgebraicCurves.Cohomology.Cech.Cover_LaurentChart_residue_mapOfRingHom
- Nyll.AlgebraicCurves.Cohomology.Cech.Cover_LaurentChart_residue_r0
- Nyll.AlgebraicCurves.Cohomology.Cech.Cover_serrePairingInt_eq_serrePairing
- Nyll.AlgebraicCurves.Cohomology.Cech.Cover_sum_residue_eq_zero_of_residueTheorem
- Nyll.AlgebraicCurves.Cohomology.Cech.OModulePresheaf_cechFinite_ofModules_of_locallyTrivial
- Nyll.AlgebraicCurves.Cohomology.Cech.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
- Nyll.AlgebraicCurves.Cohomology.Cech.OModulePresheaf_cechFinite_unit_of_isProper
- Nyll.AlgebraicCurves.Cohomology.Cech.OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
- Nyll.AlgebraicCurves.Cohomology.Cech.OModulePresheaf_nonempty_cechEquiv_ofModules_of_isQuasicoherent_of_isSeparated
- Nyll.AlgebraicCurves.Cohomology.Cech.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso
- Nyll.AlgebraicCurves.Cohomology.Cech.OModulePresheaf_nonempty_cechEquiv_ofModules_of_orderEmbedding_of_forall_lt
- Nyll.AlgebraicCurves.Cohomology.Cech.OModulePresheaf_nonempty_cechEquiv_ofModules_pullback_comap_twist_pushforwardUnit
- Nyll.AlgebraicCurves.Cohomology.Cech.OModulePresheaf_nonempty_cechEquiv_of_orderIso
- Nyll.AlgebraicCurves.Cohomology.Cech.OModulePresheaf_nonempty_cechEquiv_of_orderIso_orderDual
- Nyll.AlgebraicCurves.Cohomology.Cech.OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial
- Nyll.AlgebraicCurves.Cohomology.Cech.ProjSpaceCech_GradedModule_HMap_bijective_of_cochainMap_bijective
- Nyll.AlgebraicCurves.Cohomology.Cech.ProjSpaceCech_GradedModule_Hom_HMap_bijective_of_saturated
- Nyll.AlgebraicCurves.Cohomology.Cech.ProjSpaceCech_GradedModule_Hom_cochainMap_bijective_of_saturated
- Nyll.AlgebraicCurves.Cohomology.Cech.ProjSpaceCech_GradedModule_Hom_secMap_bijective_of_saturated
- Nyll.AlgebraicCurves.Cohomology.Cech.ProjSpaceCech_GradedModule_Hom_secMap_injective
- Nyll.AlgebraicCurves.Cohomology.Cech.ProjSpaceCech_GradedModule_Presentation_forall_H_zero_shift_eq_sec_mk_of_subsingleton_H_one
- Nyll.AlgebraicCurves.Cohomology.Cech.ProjSpaceCech_GradedModule_Presentation_subsingleton_H_of_ses
- Nyll.AlgebraicCurves.Cohomology.Cech.ProjSpaceCech_GradedModule_exists_forall_H_zero_pi_FD_shift_eq_sec_mk
- Nyll.AlgebraicCurves.Cohomology.Cech.ProjSpaceCech_GradedModule_exists_forall_H_zero_shift_eq_sec_mk_of_isFG
- Nyll.AlgebraicCurves.Cohomology.Cech.ProjSpaceCech_GradedModule_subsingleton_cohomology_shift_of_isFG
- Nyll.AlgebraicCurves.Cohomology.Cech.ProjSpaceCech_Twist_subsingleton_cohomology_of_lt
- Nyll.AlgebraicCurves.Cohomology.Cech.ProjSpaceCech_Twist_subsingleton_cohomology_of_neg_le
- Nyll.AlgebraicCurves.Cohomology.Cech.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
- Nyll.AlgebraicCurves.Cohomology.Cech.Scheme_Modules_CechTrivialisation_comap_transition
- Nyll.AlgebraicCurves.Cohomology.Cech.Scheme_Modules_CechTrivialisation_exists_forall_transition_eq_mul_mul
- Nyll.AlgebraicCurves.Cohomology.Cech.Scheme_Modules_CechTrivialisation_exists_refinement_transition_eq
- Nyll.AlgebraicCurves.Cohomology.Cech.Scheme_Modules_CechTrivialisation_isUnit_transition_and_transition_face_mul_eq
- Nyll.AlgebraicCurves.Cohomology.Cech.Scheme_Modules_CechTrivialisation_nonempty_iso_unit_of_forall_transition_eq_one
- Nyll.AlgebraicCurves.Cohomology.Cech.Scheme_Modules_ProjPresentation_exists_forall_mul_pow_le_cechFinrank_zero_tensorPow
- Nyll.AlgebraicCurves.Cohomology.Cech.Scheme_Modules_exists_orderedAffineCover_nonempty_cechTrivialisation_comap_of_isInvertible
- Nyll.AlgebraicCurves.Cohomology.Cech.Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial
- Nyll.AlgebraicCurves.Cohomology.Cech.Scheme_TwoAffineOpenCover_finrank_cechDiff_baseChange_of_isAlgClosed
- Nyll.AlgebraicCurves.Cohomology.Cech.Scheme_TwoAffineOpenCover_finrank_ker_cechDiff_baseChange_eq_one
- Nyll.AlgebraicCurves.Cohomology.Cech.Scheme_TwoAffineOpenCover_isLocallyConstant_finrank_ker_sub_finrank_coker_cechDiff_baseChange
- Nyll.AlgebraicCurves.Cohomology.Cech.SmallExtension_exists_isPicDeformationCocycle_of_cechTrivialisation
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Cover_exists_overlap_eq_sub_mem_span_of_H1_torsion_stable
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Cover_squareZeroUnit_cohomologous_iff_and_exists
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Mumford_bijective_cokerMapBaseChange
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Mumford_bijective_kerMapBaseChange
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Mumford_finite_K0
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Mumford_flat_K0
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Mumford_projective_K0
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Mumford_projective_ker_of_fibre_surjective
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Sections_finite_H0_of_chartFinite
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Sections_finite_H1_ofSubmodules_of_forall_exists_pow_mul_mem
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Sections_finite_H1_of_chartFinite
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Sections_nonempty_linearEquiv_H0_and_H1_of_linearEquiv
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_exists_fibreH0Family
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_finrank_H0_gluedLinesSections_eq_one_and_subsingleton_H1
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_finrank_H0_gluedLinesSections_of_sub_one_le_of_neg
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_finrank_H0_gluedLinesSections_zero_zero_le_one
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_finrank_H0_sub_finrank_H1_gluedLinesSections
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_finrank_ker_baseChange_eq_of_field_extension
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_gluedLinesSections_nonempty_linearEquiv_structureSheaf_iff
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_isClosed_setOf_le_finrank_ker_baseChange
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_isLocallyConstant_fibreEulerChar
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_kerMap_injective_of_H0_eq_zero
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_nonempty_kerBaseChangeTowerEquiv
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_projective_ker_of_isReduced_of_kerMapBaseChange_bijective
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_toNat_add_toNat_le_finrank_H0_gluedLinesSections_add
- Nyll.AlgebraicCurves.Cohomology.Cech.finite_ker_baseChange_of_finite_ker_of_finite_coker
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCechCupProduct
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCechLaurentChart
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCechSectionsOf
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCechSerrePairingInt
- Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_GluedLines
Imported by1
This module has no indexed declarations. Its imports and full source are available here.