All.lean
Nyll.AlgebraicCurves.Cohomology.All
0 declarations indexed from sourceView source ↗
Imports44
- Nyll.AlgebraicCurves.Cohomology.Adelic.All
- Nyll.AlgebraicCurves.Cohomology.Cech.All
- Nyll.AlgebraicCurves.Cohomology.LogDeRham
- Nyll.AlgebraicCurves.Cohomology.AdeleSpace_eq_of_genusReached
- Nyll.AlgebraicCurves.Cohomology.CechH1ToH1_bijective
- Nyll.AlgebraicCurves.Cohomology.CechH1ToH1_corrH1_of_pullback_specMap_self
- Nyll.AlgebraicCurves.Cohomology.CechH1ToH1_mk_eq_cechH1ToH1_mk_of_crossSections
- Nyll.AlgebraicCurves.Cohomology.CechH1ToH1_mk_eq_of_cechH1ToH1_pullbackAlong_mk_eq
- Nyll.AlgebraicCurves.Cohomology.CechRiemannRoch_of_genusReached
- Nyll.AlgebraicCurves.Cohomology.Exists_forall_subsingleton_cechH1_nsmul_of_degree_pos_of_riemannGenusReachedAt
- Nyll.AlgebraicCurves.Cohomology.Exists_linearEquiv_adeleSpaceQuot_H1
- Nyll.AlgebraicCurves.Cohomology.Exists_linearEquiv_cechH1_swap
- Nyll.AlgebraicCurves.Cohomology.Exists_linearEquiv_structureSheafH1_cechH1
- Nyll.AlgebraicCurves.Cohomology.Finite_H0_H1_structureSheaf_of_isAlgClosed
- Nyll.AlgebraicCurves.Cohomology.Finite_H0_H1_structureSheaf_of_smoothProperCurve
- Nyll.AlgebraicCurves.Cohomology.Finite_H1_and_exists_linearEquiv_dual_H1_omegaSpace
- Nyll.AlgebraicCurves.Cohomology.Finite_H1_of_genusReached
- Nyll.AlgebraicCurves.Cohomology.Finite_and_finrank_kaehlerSections_H0_eq_genusFF_of_isAlgClosed
- Nyll.AlgebraicCurves.Cohomology.Finrank_H0_H1_sectionsOf_of_range_eq_lSpaceOn
- Nyll.AlgebraicCurves.Cohomology.IndexOfSpecialty_eq_finrank_H1
- Nyll.AlgebraicCurves.Cohomology.Mem_adeleSpace_iff_mem_repartitions
- Nyll.AlgebraicCurves.Cohomology.Mem_principalRepartitions_iff_coe_mem_globalSub
- Nyll.AlgebraicCurves.Cohomology.Mem_repartitionsOf_iff_coe_mem_adeleBdd
- Nyll.AlgebraicCurves.Cohomology.Nonempty_linearEquiv_cechH0_and_cechH1
- Nyll.AlgebraicCurves.Cohomology.Nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf
- Nyll.AlgebraicCurves.Cohomology.Nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn
- Nyll.AlgebraicCurves.Cohomology.OModulePresheaf_exists_forall_eulerChar_baseChange_eq_of_locallyTrivial_of_isLocalRing
- Nyll.AlgebraicCurves.Cohomology.OModulePresheaf_exists_projective_complex_forall_baseChange_quasiIso_cech_of_locallyTrivial
- Nyll.AlgebraicCurves.Cohomology.OModulePresheaf_isClosed_setOf_le_cechFinrank_baseChange_residueField_of_locallyTrivial
- Nyll.AlgebraicCurves.Cohomology.OModulePresheaf_isCoherent_cechPushforward_of_isProper
- Nyll.AlgebraicCurves.Cohomology.Scheme_Modules_IsInvertible_finite_sections_of_isProper
- Nyll.AlgebraicCurves.Cohomology.Scheme_Modules_exists_norm_isInvertible_tensor_pullback_normModule_of_isFinite_of_isIntegrallyClosed
- Nyll.AlgebraicCurves.Cohomology.Scheme_Modules_finite_projective_sections_and_exists_linearEquiv_tensorProduct_pullbackLocalSection_of_forall_subsingleton_HSucc
- Nyll.AlgebraicCurves.Cohomology.SerrePairing_bijective_and_flip_bijective
- Nyll.AlgebraicCurves.Cohomology.SerrePairing_eq_of_cechH1ToH1_eq
- Nyll.AlgebraicCurves.Cohomology.SerrePairing_pullbackAlong_eq_serrePairing_traceAlong
- Nyll.AlgebraicCurves.Cohomology.SerrePairing_traceAlong_eq_serrePairing_pullbackAlong
- Nyll.AlgebraicCurves.Cohomology.SerrePairing_traceAlong_eq_serrePairing_traceAlong_pullbackAlong_of_cechH1ToH1_eq
- Nyll.AlgebraicCurves.Cohomology.WeilDualityAdelic_of_functionFieldRiemannRoch_of_stichtenothGenusExists
- Nyll.AlgebraicCurves.Cohomology.WeilDualityAdelic_of_isAlgClosed
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.All
- Nyll.AlgebraicCurves.Cohomology.SerrePairing
- Nyll.AlgebraicCurves.Cohomology.Sheaves.All
Imported by1
This module has no indexed declarations. Its imports and full source are available here.