All.lean
Nyll.AlgebraicCurves.Geometry.Curves.All
0 declarations indexed from sourceView source ↗
Imports59
- Nyll.AlgebraicCurves.Geometry.Curves.GeometricallyConnected_descendsAlong_surjective
- Nyll.AlgebraicCurves.Geometry.Curves.GeometricallyConnected_exists_fg_subalgebra_of_geometricallyConnected_pullback_snd
- Nyll.AlgebraicCurves.Geometry.Curves.GeometricallyConnected_of_comp_of_surjective
- Nyll.AlgebraicCurves.Geometry.Curves.GeometricallyIntegral_isIntegral_of_flat_of_universallyOpen
- Nyll.AlgebraicCurves.Geometry.Curves.GeometricallyIrreducible_geometricallyConnected
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_FiniteMapData_exists_baseChange
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_FiniteMapData_exists_isAffineOpen_le_preimage_of_finset
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_FiniteMapData_finite_H0_H1_sectionsOf
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_bijective_algebraMap_sections_baseChange_of_finiteMapData
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_curveModel_iso_germToFunctionField_eq_of_isAlgClosed
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_curveModel_iso_pullback_germToFunctionField_eq_of_isAlgClosed
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_curveModel_iso_pullback_of_isAlgClosed
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_curveModel_riemannRoch_of_isAlgClosed
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_finiteMapData_le_isUnit
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_finiteMapData_le_isUnit_of_twoAffineOpenCover
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_finite_etale_isClosedImmersion_le_finrank_of_finiteMapData
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_forall_le_exists_section_invModule_disjoint_of_twoAffineOpenCover
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_genus_forall_geometricFibre_riemannRoch_imp_eq_of_connectedSpace
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_genus_forall_geometricFibre_riemannRoch_imp_eq_of_finiteMapData
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_genus_forall_geometricFibre_riemannRoch_imp_eq_of_twoAffineOpenCover
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_isClosedImmersion_levelSet
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_polynomial_isUnit_aeval_imp_etale_levelSet
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_section_invModule_pow_ker_disjoint
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_section_invModule_pow_ker_notMem_support_of_isMaximal
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_section_pullback_invModule_pow_ker_notMem_support_of_twoAffineOpenCover
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_sections_injective_comp_fst_eq_comp_of_tensorProduct_algEquiv_pi
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_sections_injective_of_tensorProduct_algEquiv_pi
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_twoAffineOpenCover_mem_of_isAlgClosed
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_twoAffineOpenCover_of_section
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_forall_geometricFibre_riemannRoch_imp_eq_of_isAlgClosed
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_free_and_finrank_quotient_span_of_generates_ker_pow
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_subsingleton_H1_and_finrank_H0_sectionsOf_pullback_invModule_pow_ker
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_surjective_unit_app_top_invModule_pow_ker
- Nyll.AlgebraicCurves.Geometry.Curves.bijective_appTop_of_universallyClosed_of_geometricallyReduced_of_geometricallyConnected
- Nyll.AlgebraicCurves.Geometry.Curves.bijective_app_of_isProper_of_flat_of_geometricallyReduced_of_geometricallyConnected
- Nyll.AlgebraicCurves.Geometry.Curves.exists_smoothProperCurve_hom_comp_eq_of_ringKrullDim_eq_one
- Nyll.AlgebraicCurves.Geometry.Curves.exists_smoothProperCurve_opens_hom_comp_eq_of_ringKrullDim_eq_one
- Nyll.AlgebraicCurves.Geometry.Curves.geometricallyConnected_of_bijective_algebraMap_sections
- Nyll.AlgebraicCurves.Geometry.Curves.geometricallyConnected_of_isProper_of_bijective_appTop
- Nyll.AlgebraicCurves.Geometry.Curves.geometricallyConnected_of_isProper_of_flat_of_bijective_appTop_pullback_snd
- Nyll.AlgebraicCurves.Geometry.Curves.geometricallyConnected_of_isProper_of_flat_of_geometricallyReduced_of_geometricallyConnected_pullback_snd
- Nyll.AlgebraicCurves.Geometry.Curves.geometricallyIntegral_of_bijective_algebraMap_sections_of_smooth
- Nyll.AlgebraicCurves.Geometry.Curves.geometricallyIntegral_of_forall_isAlgClosed_isIntegral_pullback
- Nyll.AlgebraicCurves.Geometry.Curves.geometricallyIntegral_of_isAlgClosed
- Nyll.AlgebraicCurves.Geometry.Curves.geometricallyIntegral_of_smooth_of_geometricallyConnected
- Nyll.AlgebraicCurves.Geometry.Curves.isDomain_tensorProduct_sections_of_geometricallyIntegral
- Nyll.AlgebraicCurves.Geometry.Curves.isIntegral_of_smooth_of_geometricallyConnected
- Nyll.AlgebraicCurves.Geometry.Curves.mem_of_isProper_of_forall_smoothProperCurve_mem
- Nyll.AlgebraicCurves.Geometry.Curves.mem_of_isSeparated_of_forall_smoothProperCurve_opens_mem
- Nyll.AlgebraicCurves.Geometry.Curves.smooth_and_isSeparated_and_quasiCompact_and_surjective_and_geometricallyConnected_of_span_eq_top
- Nyll.AlgebraicCurves.Geometry.Curves.smooth_isProper_geometricallyConnected_of_finiteEtale_baseChange
- Nyll.AlgebraicCurves.Geometry.Curves.smooth_isSeparated_quasiCompact_geometricallyConnected_of_finiteEtale_baseChange
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurveBase
- Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurveFiniteMapData
- Nyll.AlgebraicCurves.Geometry.Curves.IsIsoOfBijectivePointsCharZero
- Nyll.AlgebraicCurves.Geometry.Curves.GeometricGenus
- Nyll.AlgebraicCurves.Geometry.Curves.GeometricGenusBaseChange
Imported by1
This module has no indexed declarations. Its imports and full source are available here.