All.lean
Nyll.AlgebraicCurves.Models.All
0 declarations indexed from sourceView source ↗
Imports95
- Nyll.AlgebraicCurves.Models.Basic
- Nyll.AlgebraicCurves.Models.ChartAlgebra
- Nyll.AlgebraicCurves.Models.Construction
- Nyll.AlgebraicCurves.Models.Gluing.All
- Nyll.AlgebraicCurves.Models.Places
- Nyll.AlgebraicCurves.Models.CurveModel_apply_genericPoint_eq_and_nonempty_algEquiv_functionField_of_isIso_stalkMap
- Nyll.AlgebraicCurves.Models.CurveModel_coe_mem_and_sub_algebraMap_mem_nonunits_of_range_stalk_eq_iota0
- Nyll.AlgebraicCurves.Models.CurveModel_coe_mem_and_sub_algebraMap_mem_nonunits_of_range_stalk_eq_iotaInf
- Nyll.AlgebraicCurves.Models.CurveModel_dense_range_isPullback_lift_specMap_comp_point
- Nyll.AlgebraicCurves.Models.CurveModel_eq_genusFF_of_forall_ell_sub_ell_eq
- Nyll.AlgebraicCurves.Models.CurveModel_eq_pointEquivPlace_of_forall_ffEquiv_symm_germToFunctionField_sub_algebraMap_mem_nonunits_of_baseChange
- Nyll.AlgebraicCurves.Models.CurveModel_eq_pointEquivPlace_of_forall_ffEquiv_symm_germToFunctionField_sub_algebraMap_mem_nonunits_of_isClosedImmersion
- Nyll.AlgebraicCurves.Models.CurveModel_existsUnique_point_and_ord_eq_and_ord_eq_zero_of_iso_pullback_of_ffEquiv_symm_germToFunctionField_eq
- Nyll.AlgebraicCurves.Models.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
- Nyll.AlgebraicCurves.Models.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
- Nyll.AlgebraicCurves.Models.CurveModel_exists_comp_toBase_eq_id_and_base_closedPoint_eq_of_deg_eq_one
- Nyll.AlgebraicCurves.Models.CurveModel_exists_curveModel_hom_pullback_pullback_germ_eq_of_ringEquiv_functionField
- Nyll.AlgebraicCurves.Models.CurveModel_exists_curveModel_iso_ffEquiv_symm_germToFunctionField_eq_of_algEquiv
- Nyll.AlgebraicCurves.Models.CurveModel_exists_curveModel_iso_of_algEquiv
- Nyll.AlgebraicCurves.Models.CurveModel_exists_curveModel_ratFunc
- Nyll.AlgebraicCurves.Models.CurveModel_exists_divisorClassMap
- Nyll.AlgebraicCurves.Models.CurveModel_exists_eq_appTop_of_isUnit
- Nyll.AlgebraicCurves.Models.CurveModel_exists_finite_flat_hom_of_algHom
- Nyll.AlgebraicCurves.Models.CurveModel_exists_hom_of_algHom
- Nyll.AlgebraicCurves.Models.CurveModel_exists_hom_pointEquivPlace_restrict_eq
- Nyll.AlgebraicCurves.Models.CurveModel_exists_iso_comp_toBase_eq_placeOfPoint_congr_eq
- Nyll.AlgebraicCurves.Models.CurveModel_exists_iso_fromSpecStalk_comp_eq_and_pointEquivPlace_symm_comp_eq_of_algEquiv
- Nyll.AlgebraicCurves.Models.CurveModel_exists_iso_of_twoAffineLineCover
- Nyll.AlgebraicCurves.Models.CurveModel_exists_opens_hom_comp_eq_of_existsUnique_evalAt_eq_appLE
- Nyll.AlgebraicCurves.Models.CurveModel_exists_ringHom_functionField_ffEquiv_symm_stalkMap_eq_of_isIso_pullback
- Nyll.AlgebraicCurves.Models.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
- Nyll.AlgebraicCurves.Models.CurveModel_ffEquiv_symm_germToFunctionField_mem_and_sub_algebraMap_appLE_mem_nonunits_pointEquivPlace
- Nyll.AlgebraicCurves.Models.CurveModel_ffEquiv_symm_germToFunctionField_sub_algebraMap_mem_nonunits_pointEquivPlace_of_comp_eq_specMap_comp
- Nyll.AlgebraicCurves.Models.CurveModel_ffEquiv_symm_mem_and_evalAt_pointEquivPlace_eq_stalkClosedPointTo
- Nyll.AlgebraicCurves.Models.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
- Nyll.AlgebraicCurves.Models.CurveModel_finite_integralClosure_sections_of_isIso_stalkMap
- Nyll.AlgebraicCurves.Models.CurveModel_finrank_H0_sectionsOf_invModule_prod_ker_tensor_module_prod_ker_eq_ell
- Nyll.AlgebraicCurves.Models.CurveModel_finrank_H1_sectionsOf_unit_eq_zero_and_finrank_H0_eq_one_of_ratFunc
- Nyll.AlgebraicCurves.Models.CurveModel_germ_app_eq_of_germ_eq_of_comp_eq_comp_of_fromSpecStalk_comp_eq
- Nyll.AlgebraicCurves.Models.CurveModel_hasValue_placeOfPoint_of_sub_algebraMap_mem
- Nyll.AlgebraicCurves.Models.CurveModel_infinite_place
- Nyll.AlgebraicCurves.Models.CurveModel_irreducibleSpace_and_topologicalKrullDim_pullback_eq_one
- Nyll.AlgebraicCurves.Models.CurveModel_isFinite_and_flat_and_locallyOfFinitePresentation_and_surjective_of_pointEquivPlace_comp_eq_restrictAlong
- Nyll.AlgebraicCurves.Models.CurveModel_isFinite_of_isIso_stalkMap
- Nyll.AlgebraicCurves.Models.CurveModel_isProper_smooth_places_affineCover_glued
- Nyll.AlgebraicCurves.Models.CurveModel_isRational_pointEquivPlace
- Nyll.AlgebraicCurves.Models.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
- Nyll.AlgebraicCurves.Models.CurveModel_natCard_stabilizer_pointEquivPlace_mul_natCard_ker_eq
- Nyll.AlgebraicCurves.Models.CurveModel_nonempty_of_perfectField
- Nyll.AlgebraicCurves.Models.CurveModel_nonempty_pullback_foldr_ofPoint_pow_iso_foldr_ofPoint_pointEquivPlace_symm_of_pointEquivPlace_comp_eq_restrictAlong
- Nyll.AlgebraicCurves.Models.CurveModel_nonempty_pullback_ofPoint_module_iso_foldr_pow_ramificationIndexAlong_of_pointEquivPlace_comp_eq_restrictAlong
- Nyll.AlgebraicCurves.Models.CurveModel_ord_placeOfPoint_ffEquiv_symm_algebraMap_eq_one_of_maximalIdeal_eq_span
- Nyll.AlgebraicCurves.Models.CurveModel_ord_placeOfPoint_ffEquiv_symm_germToFunctionField_eq_zero_of_isUnit
- Nyll.AlgebraicCurves.Models.CurveModel_placeOfPoint_ofGenerator_iota0_comap
- Nyll.AlgebraicCurves.Models.CurveModel_placeOfPoint_ofGenerator_iotaInf_comap
- Nyll.AlgebraicCurves.Models.CurveModel_place_eq_of_pointEquivPlace_symm_comp_eq
- Nyll.AlgebraicCurves.Models.CurveModel_pointEquivPlace_comp_eq_congrRingEquiv_of_fromSpecStalk_comp_eq
- Nyll.AlgebraicCurves.Models.CurveModel_pointEquivPlace_eq_smul_pointEquivPlace_of_fromSpecStalk_comp_eq_of_apply_closedPoint_eq
- Nyll.AlgebraicCurves.Models.CurveModel_ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified
- Nyll.AlgebraicCurves.Models.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
- Nyll.AlgebraicCurves.Models.CurveModel_sub_algebraMap_mem_of_hasValue_placeOfPoint
- Nyll.AlgebraicCurves.Models.CurveModel_sum_mul_eq_zero_of_sum_mul_eq_zero_of_dense_of_germ_eq
- Nyll.AlgebraicCurves.Models.CurveModel_surjective_and_eq_genericPoint_or_isClosed_singleton_of_isIso_stalkMap
- Nyll.AlgebraicCurves.Models.Eq_of_range_stalk_eq
- Nyll.AlgebraicCurves.Models.Exists_closedPoint_range_stalk_eq
- Nyll.AlgebraicCurves.Models.Exists_curveModel_iso_of_algEquiv_functionField
- Nyll.AlgebraicCurves.Models.Exists_isAffineOpen_forall_mem_and_finite_compl
- Nyll.AlgebraicCurves.Models.Exists_isAffineOpen_forall_mem_of_finset
- Nyll.AlgebraicCurves.Models.Exists_isAffineOpen_forall_mem_of_finset_of_field
- Nyll.AlgebraicCurves.Models.Exists_isAffineOpen_sup_eq_top
- Nyll.AlgebraicCurves.Models.Exists_isFinite_hom_proj_of_isProper
- Nyll.AlgebraicCurves.Models.Exists_transcendental_mem_range_stalk_iff_ne
- Nyll.AlgebraicCurves.Models.Finite_compl_of_isOpen
- Nyll.AlgebraicCurves.Models.GermToFunctionField_app_eq_of_fromSpecStalk_comp_eq
- Nyll.AlgebraicCurves.Models.IsAffineOpen_of_maximal_domain
- Nyll.AlgebraicCurves.Models.IsCurveOver_of_isIntegral_of_smoothOfRelativeDimension_one
- Nyll.AlgebraicCurves.Models.IsCurveOver_of_ringEquiv_functionField_of_isIntegral_of_smoothOfRelativeDimension_one
- Nyll.AlgebraicCurves.Models.Not_isAffine_of_isProper_of_isCurveOver
- Nyll.AlgebraicCurves.Models.Range_algebraMap_functionField_eq_iInf_of_isAffineOpen
- Nyll.AlgebraicCurves.Models.Smoothness
- Nyll.AlgebraicCurves.Models.Transport
- Nyll.AlgebraicCurves.Models.CurveModel_baseChange_semilinearAction
- Nyll.AlgebraicCurves.Models.CurveModelSemilinearFixedField
- Nyll.AlgebraicCurves.Models.CurveModelGenericPointEvaluation
- Nyll.AlgebraicCurves.Models.CurveModelGeometricGenericLift
- Nyll.AlgebraicCurves.Models.FiniteEtaleRiemannHurwitz
- Nyll.AlgebraicCurves.Models.FiniteEtaleHyperbolicGenus
- Nyll.AlgebraicCurves.Models.RationalPointExistence
- Nyll.AlgebraicCurves.Models.FunctionFieldScalarFunctoriality
- Nyll.AlgebraicCurves.Models.EtaleLocalRootDivisibility
- Nyll.AlgebraicCurves.Models.OpenBoundary
- Nyll.AlgebraicCurves.Models.OpenInteriorRamification
- Nyll.AlgebraicCurves.Models.FiniteCurveBoundaryMap
- Nyll.AlgebraicCurves.Models.OpenCoverRiemannHurwitz
- Nyll.AlgebraicCurves.Models.FunctionFieldModPH2
Imported by1
This module has no indexed declarations. Its imports and full source are available here.