← all areas

Namespace NeronModelInfra 96 theorems

— 76 · ComponentReading 5 · MinimalComponentData 1 · NeronModelPropertyBundle 3 · TopFormOrder 11

directly in NeronModelInfra 76

• Extending generic-fibre endomorphisms over mathbf Z_{(ℓ)} NeronModelInfra.exists_extension_baseChange_ratLocalizedAt_of_genericFibre 39 below · cited by 1 · depth 15
• Extending generic-fibre morphisms is local on the base NeronModelInfra.existsUnique_extension_of_exists_isLocalization_atPrime 1 below · cited by 2 · depth 16
• Global extension of a homomorphic endomorphism of G_ℚ NeronModelInfra.exists_extension_hom_of_forall_isMaximal_of_relativeGroupLaw 3 below · cited by 1 · depth 16
• Extending an endomorphism of G_ℚ over mathbb Z₍ₚ₎ NeronModelInfra.exists_extension_pullback_of_opens_extension_of_relativeGroupLaw 26 below · cited by 1 · depth 16
• Injectivity of restriction to the generic fibre NeronModelInfra.genericFibreRestrict_injective_of_flat_of_isSeparated 0 below · cited by 14 · depth 16
• Néron mapping property from the quasi-compact case NeronModelInfra.neronUniqueExtension_of_forall_quasiCompact 1 below · cited by 3 · depth 16
• Extension over an open meeting every component of the special fibre NeronModelInfra.exists_opens_extension_of_isProper_of_smooth 7 below · cited by 1 · depth 17
• Extension across a maximal point of the special fibre NeronModelInfra.exists_nhds_extension_of_isProper_of_smooth 5 below · cited by 1 · depth 18
• Néron mapping property from extendability of K-points NeronModelInfra.neronModelPropertyBundle_of_surjective_genericFibreRestrict_of_henselian 47 below · cited by 1 · depth 19
• Néron criterion, local step: extension near a maximal point NeronModelInfra.exists_nhds_extension_of_surjective_genericFibreRestrict_of_smooth 20 below · cited by 1 · depth 20
• Gluing neighbourhood extensions over a discrete valuation ring NeronModelInfra.exists_opens_extension_of_forall_nhds_extension 1 below · cited by 4 · depth 20
• Valuative criterion of properness over a valuation subring NeronModelInfra.existsUnique_schemeHomOver_comp_eq_of_isProper_valuationSubring 0 below · cited by 6 · depth 26
• Proper K-schemes have finite index-one-catching R-model families NeronModelInfra.exists_modelFamily_finite_catchesIndexOnePoints_of_isProper 1 below · cited by 1 · depth 28
• Smooth group model with extending twisted translations (commutative case) NeronModelInfra.exists_relativeGroupLaw_genericFibre_iso_nhds_twist_extension_of_catchesIndexOnePoints_of_henselianLocalRing_of_isCommutative 215 below · cited by 1 · depth 28
• Néron smoothening over a discrete valuation ring NeronModelInfra.exists_smooth_hom_isIso_genericFibre_lift_of_isIndexOneExtension 42 below · cited by 1 · depth 28
• Néron mapping property from local extension of twisted maps NeronModelInfra.neronModelPropertyBundle_of_forall_nhds_twist_extension 29 below · cited by 1 · depth 28
• Uniform bound for Néron's defect of smoothness NeronModelInfra.exists_forall_smoothnessDefect_le_of_smooth_pullback_snd 0 below · cited by 1 · depth 29
• One smoothening step lowering the defect of smoothness NeronModelInfra.exists_hom_isIso_smoothnessDefect_add_one_le_of_smooth_pullback_snd 40 below · cited by 1 · depth 29
• Translation-extending R-model from a weak Néron model, commutative case NeronModelInfra.exists_model_forall_nhds_translation_extension_isOpenImmersion_of_catchesIndexOnePoints_of_isCommutative 129 below · cited by 1 · depth 29
• Generic fibre group law extends to R-birational group law NeronModelInfra.exists_opens_mul_extension_isOpenImmersion_lift_of_forall_nhds_translation_extension 2 below · cited by 1 · depth 29
• Birational group law over a henselian DVR has a solution NeronModelInfra.exists_opens_relativeGroupLaw_isOpenImmersion_genericFibre_iso_of_isOpenImmersion_lift_mul_of_henselianLocalRing 92 below · cited by 1 · depth 29
• Vanishing of Néron's smoothness defect at a discrete-valuation-ring point NeronModelInfra.smoothnessDefect_eq_zero_iff_apply_closedPoint_mem_smoothLocus 3 below · cited by 2 · depth 29
• Permissible stratification of the non-smooth index-one specialisations NeronModelInfra.exists_antitone_isClosed_forall_indexOne_chart_of_smooth_pullback_snd 9 below · cited by 1 · depth 30
• Simultaneous dilatation along a descending chain of closed strata NeronModelInfra.exists_hom_isIso_morphismRestrict_compl_iso_affineDilatation_of_antitone_isClosed 6 below · cited by 1 · depth 30
• Existence of ω-minimal component data over a discrete valuation ring NeronModelInfra.exists_minimalComponentData_isOmegaMinimal_of_catchesIndexOnePoints 59 below · cited by 1 · depth 30
• Gluing pairwise inequivalent smooth R-models into one model NeronModelInfra.exists_model_openCover_of_forall_ne_not_exists_extension 18 below · cited by 1 · depth 30
• Strict birational group law on a dense open subscheme NeronModelInfra.exists_opens_forall_dense_preimage_fibre_of_isOpenImmersion_lift_mul 5 below · cited by 1 · depth 30
• Strict birational group laws over henselian discrete valuation rings NeronModelInfra.exists_relativeGroupLaw_isOpenImmersion_opens_of_forall_dense_preimage_fibre_of_henselianLocalRing 85 below · cited by 1 · depth 30
• Translation extension at maximal special points of Z×_R X NeronModelInfra.forall_nhds_translation_extension_isOpenImmersion_of_isOmegaMinimal_of_openCover_of_isCommutative 70 below · cited by 1 · depth 30
• Smoothness defect drops under an affine dilatation NeronModelInfra.smoothnessDefect_affineDilatation_add_one_le_of_isSmoothAt_of_mem_freeLocus 21 below · cited by 1 · depth 30
• Existence of an ω-reading at a maximal special-fibre point NeronModelInfra.exists_componentReading_data_of_smooth_of_forall_specializes 23 below · cited by 2 · depth 31
• Strict birational group law solved after finite étale base change NeronModelInfra.exists_finite_etale_relativeGroupLaw_isOpenImmersion_of_forall_dense_preimage_fibre_of_henselianLocalRing 36 below · cited by 1 · depth 31
• Dilatation of a closed subset of the special fibre NeronModelInfra.exists_isAffineHom_isIso_morphismRestrict_iso_affineDilatation_of_isClosed 5 below · cited by 1 · depth 31
• Extending an R-model across the generic fibre NeronModelInfra.exists_isOpenImmersion_model_isIso_genericFibre_of_isOpenImmersion_chart 1 below · cited by 1 · depth 31
• Dense slices near a maximal point of the special fibre NeronModelInfra.exists_mem_opens_forall_dense_preimage_fst_of_forall_maximal_mem 4 below · cited by 1 · depth 31
• Gluing smooth R-models along a common generic fibre NeronModelInfra.exists_model_openCover_of_forall_isClosedImmersion_pullback_lift 1 below · cited by 1 · depth 31
• Minimal order and formal smoothness at a maximal special point NeronModelInfra.exists_n_eq_and_formallySmooth_stalk_of_isOmegaMinimal_of_genericFibreRestrict_comp_eq_mul 52 below · cited by 1 · depth 31
• Neighbourhood extension into a family catching index-one points NeronModelInfra.exists_nhds_extension_chart_of_catchesIndexOnePoints 13 below · cited by 2 · depth 31
• Formally smooth birational translation extends to an open immersion NeronModelInfra.exists_nhds_translation_extension_isOpenImmersion_of_formallySmooth_stalk_of_isOmegaMinimal 18 below · cited by 1 · depth 31
• Shrinking inequivalent smooth models so diagonals become closed immersions NeronModelInfra.exists_opens_forall_isClosedImmersion_of_forall_ne_not_exists_extension 15 below · cited by 1 · depth 31
• Openness of the smooth–free stratum on an affine chart NeronModelInfra.exists_opens_inter_closure_eq_setOf_isSmoothAt_and_mem_freeLocus 6 below · cited by 1 · depth 31
• Finite étale descent of a birational group law solution NeronModelInfra.exists_relativeGroupLaw_isOpenImmersion_opens_of_finite_etale_relativeGroupLaw_isOpenImmersion_of_henselianLocalRing 61 below · cited by 1 · depth 31
• Lifting generisations along slices of X×_R X NeronModelInfra.exists_specializes_fst_eq_snd_eq_of_specializes_snd 0 below · cited by 2 · depth 31
• Maximal points of the special fibre of a smooth model over a DVR NeronModelInfra.finite_maximal_specialFibre_and_existsUnique_specializes_and_exists_opens 9 below · cited by 2 · depth 31
• Translation by a K-point is birational at η NeronModelInfra.isFractionRing_stalk_of_genericFibreRestrict_comp_eq_mul_of_pullback_lift 6 below · cited by 2 · depth 31
• Smoothness and freeness transfer to a basic open sub-chart NeronModelInfra.isSmoothAt_and_mem_freeLocus_basicOpen_of_isSmoothAt_of_mem_freeLocus 0 below · cited by 1 · depth 31
• The inclusion I ⊆ J² in Néron's smoothening NeronModelInfra.le_sq_of_linearIndependent_tmul_D_of_forall_indexOne 0 below · cited by 1 · depth 31
• Index-one points detect the vanishing ideal of S̄ NeronModelInfra.mem_vanishingIdeal_closure_of_forall_indexOne_algHom 1 below · cited by 1 · depth 31
• Points of a local scheme factor through an affine chart NeronModelInfra.exists_algHom_comap_maximalIdeal_eq_primeIdealOf_of_apply_closedPoint_mem 0 below · cited by 2 · depth 32
• Descent action on a solution of a birational group law NeronModelInfra.exists_descentAction_of_finite_etale_relativeGroupLaw_isOpenImmersion_of_henselianLocalRing 28 below · cited by 1 · depth 32
• Finite étale solution of a strict birational group law NeronModelInfra.exists_finite_etale_isOpenImmersion_forall_mem_of_mem_range_of_forall_dense_preimage_fibre_of_henselianLocalRing 33 below · cited by 1 · depth 32
• Landing a translate in X from a chart on an ω-minimal component NeronModelInfra.exists_nhds_translation_extension_isOpenImmersion_of_isOpenImmersion_homOfLE_comp_of_isOmegaMinimalRep 0 below · cited by 1 · depth 32
• Descent of a solution of a birational group law along R'/R NeronModelInfra.exists_relativeGroupLaw_isOpenImmersion_opens_of_effective_descentAction_of_finite_etale_relativeGroupLaw_isOpenImmersion 1 below · cited by 1 · depth 32
• Strict birational group law yields a relative group law NeronModelInfra.exists_relativeGroupLaw_mul_eq_of_forall_dense_preimage_fibre_of_forall_mem_opens_of_section 3 below · cited by 1 · depth 32
• Stalk at a generic point of the special fibre: index one NeronModelInfra.isIndexOneExtension_stalk_of_smooth_of_forall_specializes 9 below · cited by 5 · depth 32
• Translated point: the chart of τ₀ computes a· x NeronModelInfra.mul_pointGenericFibre_eq_pointGenericFibre_comp_chart_of_genericFibreRestrict_comp_eq_mul 0 below · cited by 1 · depth 32
• Closure of the generic diagonal misses the special fibre's generic point NeronModelInfra.not_mem_closure_image_fst_closure_range_of_forall_not_exists_extension 14 below · cited by 1 · depth 32
• Finite étale extension gluing translates of a birational group law NeronModelInfra.exists_finite_etale_isOpenImmersion_forall_exists_translation_of_forall_dense_preimage_fibre_of_henselianLocalRing 28 below · cited by 1 · depth 33
• Restricting a birational group law to an open subscheme NeronModelInfra.exists_forall_dense_preimage_fibre_comp_eq_comp_of_forall_dense_preimage_fibre_of_relativeGroupLaw 2 below · cited by 1 · depth 33
• Birational group law with a section extends to the product NeronModelInfra.exists_mul_extension_isIso_lift_of_forall_dense_preimage_fibre_of_forall_mem_opens_of_section 2 below · cited by 1 · depth 33
• Enlarging the domain of m' over a henselian base NeronModelInfra.exists_opens_forall_mem_of_mem_range_of_forall_exists_translation_of_henselianLocalRing 23 below · cited by 1 · depth 33
• Closure of the generic diagonal misses ξ₁ (integral case) NeronModelInfra.not_mem_closure_image_fst_closure_range_of_forall_not_exists_extension_of_isIntegral 12 below · cited by 1 · depth 33
• One glued translate over a faithfully flat extension NeronModelInfra.exists_glue_translate_baseChange_isOpenImmersion_forall_range_subset_of_forall_dense_preimage_fibre 17 below · cited by 1 · depth 34
• Extending the generic-fibre map near a special point NeronModelInfra.exists_nhds_extension_of_isIso_stalkMap_imageInc_fst 1 below · cited by 1 · depth 34
• Translated birational group law descends to an open domain NeronModelInfra.exists_opens_forall_range_subset_of_comp_translation_eq_of_etale 2 below · cited by 1 · depth 34
• Stalk isomorphism for the first projection on the schematic image NeronModelInfra.isIso_stalkMap_imageInc_fst_of_fst_eq 6 below · cited by 1 · depth 34
• Strict birational group laws extend to larger open domains NeronModelInfra.isOpenImmersion_lift_and_forall_comp_eq_of_homOfLE_comp_eq_of_forall_dense_preimage_fibre 11 below · cited by 1 · depth 34
• Scheme-theoretic image of the generic-fibre diagonal over a DVR NeronModelInfra.isOpenImmersion_toImage_and_range_toImage_and_range_imageInc_of_genericFibre 0 below · cited by 1 · depth 34
• Graph closure of a birational group law over a DVR NeronModelInfra.exists_isClosedImmersion_range_eq_closure_isOpenImmersion_of_forall_dense_preimage_fibre 10 below · cited by 2 · depth 35
• Gluing a smooth R-scheme to its translate by a section NeronModelInfra.exists_isSeparated_isOpenImmersion_isPullback_glue_translate_of_isClosedImmersion_of_section 2 below · cited by 1 · depth 35
• Strict birational group laws descend along base change NeronModelInfra.exists_lift_forall_dense_preimage_fibre_of_isPullback_of_forall_dense_preimage_fibre 0 below · cited by 1 · depth 35
• Strict birational group law extends along a translate gluing NeronModelInfra.exists_opens_forall_dense_preimage_fibre_of_isPullback_glue_translate_of_section 11 below · cited by 1 · depth 35
• Field-valued points of a birational group law graph closure NeronModelInfra.eq_of_comp_eq_of_range_subset_closure_range_lift_of_forall_dense_preimage_fibre 3 below · cited by 1 · depth 36
• Birational group law on a glued translate, with quasi-finite translations NeronModelInfra.exists_opens_locallyQuasiFinite_forall_exists_comp_eq_of_glue_translate_of_section 2 below · cited by 1 · depth 36
• Fibrewise density of U' and its translations after gluing NeronModelInfra.forall_dense_preimage_fibre_of_forall_exists_comp_eq_glue_translate 0 below · cited by 1 · depth 36
• Strictness and associativity descend to a quasi-finite extension of m NeronModelInfra.isOpenImmersion_lift_and_forall_comp_eq_of_locallyQuasiFinite_of_forall_exists_comp_eq 8 below · cited by 1 · depth 36

NeronModelInfra.ComponentReading 5

• Order comparison along a chart-compatible morphism of ω-readings NeronModelInfra.ComponentReading.n_le_n_and_isOpenImmersion_of_n_eq_of_specializes 45 below · cited by 1 · depth 31
• Value of ω at an F-point specialising through y₁ NeronModelInfra.ComponentReading.exists_basis_units_topFormMap_eq_mul_zpow_smul_of_specializes 38 below · cited by 2 · depth 32
• Stalk birationality along a chart-compatible morphism of readings NeronModelInfra.ComponentReading.isDomain_and_injective_stalkMap_and_isScalarTower_and_isFractionRing_of_chart_comp_eq 4 below · cited by 1 · depth 32
• Local exponent of ω at a closed-fibre point equals T.n NeronModelInfra.ComponentReading.eq_n_of_forall_topFormMap_eq_mul_zpow_smul 16 below · cited by 1 · depth 33
• Laurent form of ω at a special point of a reading NeronModelInfra.ComponentReading.exists_basis_units_int_forall_topFormMap_eq_mul_zpow_smul_of_specializes 26 below · cited by 1 · depth 33

NeronModelInfra.MinimalComponentData 1

• A maximal special point of a glued model comes from one component NeronModelInfra.MinimalComponentData.exists_ringHom_stalk_chart_comp_eq_pointGenericFibre_of_forall_specializes 0 below · cited by 1 · depth 32

NeronModelInfra.NeronModelPropertyBundle 3

• Abelian schemes over a DVR satisfy the Néron property bundle NeronModelInfra.NeronModelPropertyBundle.of_abelianSchemePropertyBundle 34 below · cited by 8 · depth 15
• K-points of the generic fibre lift to R-sections NeronModelInfra.NeronModelPropertyBundle.exists_section_comp_eq 0 below · cited by 3 · depth 20
• Abelian open subscheme of a Néron model is everything NeronModelInfra.NeronModelPropertyBundle.isIso_and_abelianSchemePropertyBundle_of_isOpenImmersion 35 below · cited by 1 · depth 29

NeronModelInfra.TopFormOrder 11

• Order squeeze forcing equality and bijective differential base change NeronModelInfra.TopFormOrder.eq_addOrd_and_bijective_mapBaseChange_of_topFormMap_eq_of_addOrd_le 7 below · cited by 1 · depth 32
• Integral top forms cyclic on a basis wedge; ord(aρ)=ord(a) NeronModelInfra.TopFormOrder.integralTopForms_eq_span_and_ord_smul_of_basis 0 below · cited by 5 · depth 32
• Order of uvarpi^mρ' downstairs: equality iff base change bijective NeronModelInfra.TopFormOrder.le_ord_and_ord_eq_iff_bijective_mapBaseChange_of_eq_unit_mul_zpow_smul 4 below · cited by 3 · depth 32
• Top differential forms over F form the line spanned by ρ NeronModelInfra.TopFormOrder.topFormMap_iotaMulti_ne_zero_and_forall_exists_smul_eq 0 below · cited by 5 · depth 32
• Non-vanishing of a free top form in the differentials of a localisation NeronModelInfra.TopFormOrder.topFormMap_ne_zero_of_bijective_smul_of_isLocalization 0 below · cited by 1 · depth 32
• Functoriality of `topFormMap` along a tower of algebras NeronModelInfra.TopFormOrder.topFormMap_topFormMap 0 below · cited by 8 · depth 32
• Normalised order on a DVR: additivity, non-negativity, units, uniformisers NeronModelInfra.TopFormOrder.addOrd_mul_and_nonneg_and_eq_zero_iff_and_uniformizer 0 below · cited by 2 · depth 33
• Comparison of integral top forms along O'→ O NeronModelInfra.TopFormOrder.exists_det_topFormMap_eq_smul_and_isUnit_iff_bijective_mapBaseChange 0 below · cited by 1 · depth 33
• Invariance of the order of a top form under index-one base change NeronModelInfra.TopFormOrder.ord_topFormMap_eq_ord_of_map_maximalIdeal_eq 2 below · cited by 1 · depth 33
• Uniform Laurent form of a generating top differential form NeronModelInfra.TopFormOrder.exists_basis_units_int_forall_topFormMap_eq_mul_zpow_smul_of_span_singleton_eq_top 3 below · cited by 1 · depth 34
• Basis wedge generates top forms after inverting varpi NeronModelInfra.TopFormOrder.span_topFormMap_iotaMulti_eq_top_and_exists_units_eq_smul_of_isLocalization_away 0 below · cited by 1 · depth 35