All.lean
Nyll.AlgebraicCurves.Geometry.Projective.All
0 declarations indexed from sourceView source ↗
Imports43
- Nyll.AlgebraicCurves.Geometry.Projective.ProjTwistDatum
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_app_awayToSection_linearForm_mul_eq_zero_imp_of_forall_mul_mem_imp
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_affSES_twist_succ_of_forall_mul_eq_zero_imp
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_algHom_away_apply_ratio_eq
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_fg_subalgebra_isClosedImmersion_flat_isPullback_comp_map_of_isClosedImmersion_of_flat_of_locallyOfFinitePresentation
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_forall_H0_twist_exists_isHomogeneous_forall_val_eq_of_isClosedImmersion
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_forall_awayToSection_mk_X_pow_mul_mem_ideal_of_mem_ideal
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_forall_mem_grade_exists_isHomogeneous_forall_apply_eq_of_isClosedImmersion
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_forall_subsingleton_HSucc_twist
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_hom_twist_val_eq_mul_and_injective_of_cocycle
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_isClosedImmersion_isPullback_comp_eq_map
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_isFG_hom_injective_saturated_twistGradedModule
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_iso_hom_comp_eq_of_isPullback_of_comp_eq_map
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_polynomial_natDegree_le_forall_finrank_H0_twist_eq_of_forall_subsingleton_HSucc
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_sec_shift_twistGradedModule_equiv
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_twistObj_top_forall_res_eq_of_mem_H0_twist
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_finite_H0_twist_and_finite_HSucc_twist_of_isClosedImmersion
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_finite_projective_H0_twist_of_ker_baseChange_of_isPullback
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_forall_H0_twist_exists_of_forall_subsingleton_HSucc_of_maximal_growth
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_forall_subsingleton_HSucc_twist_and_forall_H0_exists_of_finrank_piece_eq_zero
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_isCoherent_twist_and_flat
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_isPullback_comp_and_comp_eq_map_of_isScalarTower
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_isQuasicoherent_twist
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_ker_baseChange_le_range_and_finrank_ker_eq_of_point_of_isPullback
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_mem_map_iff_forall_app_awayToSection_eq_zero_of_baseChange_field
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_restrictFun_app_app_awayToSection_eq_app_awayToSection_map
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_subsingleton_HSucc_twist_of_subsingleton_HSucc_twist_baseChange_field
- Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_topologicalKrullDim_le_of_isClosedImmersion
- Nyll.AlgebraicCurves.Geometry.Projective.Scheme_Modules_isInvertible_tilde_of_projective_rankOne
- Nyll.AlgebraicCurves.Geometry.Projective.Scheme_Modules_projective_sections_of_locallyTrivial
- Nyll.AlgebraicCurves.Geometry.Projective.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
- Nyll.AlgebraicCurves.Geometry.Projective.Scheme_TwoAffineOpenCover_sectionsOf_isInvertible_projective_finite_finrank
Imported by1
This module has no indexed declarations. Its imports and full source are available here.