All.lean
Nyll.AlgebraicCurves.Geometry.Schemes.All
0 declarations indexed from sourceView source ↗
Imports279
- Nyll.AlgebraicCurves.Geometry.Schemes.AffineLimit
- Nyll.AlgebraicCurves.Geometry.Schemes.FGSubalgebraTensorStage
- Nyll.AlgebraicCurves.Geometry.Schemes.Kmf2FiberSpecTensorStalkLeg1AffineDatum
- Nyll.AlgebraicCurves.Geometry.Schemes.SmoothRelativeDimension
- Nyll.AlgebraicCurves.Geometry.Schemes.MumfordTruncation
- Nyll.AlgebraicCurves.Geometry.Schemes.OrderedAffineCoverComap
- Nyll.AlgebraicCurves.Geometry.Schemes.AffineLimit_homIsLFP_of_locallyOfFinitePresentation
- Nyll.AlgebraicCurves.Geometry.Schemes.AffineLimit_locallyOfFiniteType_of_forall_exists_fg_factor
- Nyll.AlgebraicCurves.Geometry.Schemes.AffineLimit_presheafULift_isOpenImmersion_and_isLocallySurjective_of_locallyOfFiniteType
- Nyll.AlgebraicCurves.Geometry.Schemes.FGSubalgebra_nonempty_isColimit_cocone
- Nyll.AlgebraicCurves.Geometry.Schemes.FGSubalgebra_nonempty_isLimit_specCone
- Nyll.AlgebraicCurves.Geometry.Schemes.Flat_exists_fg_subalgebra_of_flat_pullback_snd
- Nyll.AlgebraicCurves.Geometry.Schemes.FormallyUnramified_eq_of_comp_eq_of_isLocalRing
- Nyll.AlgebraicCurves.Geometry.Schemes.GeometricallyReduced_of_isReduced_of_perfectField
- Nyll.AlgebraicCurves.Geometry.Schemes.IsAffineOpen_eq_of_appLE_eq_and_exists_appLE_eq_of_ringHom
- Nyll.AlgebraicCurves.Geometry.Schemes.IsAffineOpen_range_algebraMap_functionField_eq_iInf
- Nyll.AlgebraicCurves.Geometry.Schemes.IsAffineOpen_ringKrullDim_stalk_le
- Nyll.AlgebraicCurves.Geometry.Schemes.IsClosedImmersion_app_curveChange_injective_and_exists_of_app_eq_of_isReduced
- Nyll.AlgebraicCurves.Geometry.Schemes.IsClosedImmersion_app_injective_and_exists_of_app_pullback_eq_of_isAffineOpen
- Nyll.AlgebraicCurves.Geometry.Schemes.IsClosedImmersion_app_injective_and_exists_of_app_pullback_eq_of_isReduced
- Nyll.AlgebraicCurves.Geometry.Schemes.IsClosedImmersion_existsUnique_comp_eq_of_range_subset_of_isReduced
- Nyll.AlgebraicCurves.Geometry.Schemes.IsClosedImmersion_exists_fg_subalgebra_of_isClosedImmersion_pullback_map
- Nyll.AlgebraicCurves.Geometry.Schemes.IsClosedImmersion_exists_fg_subalgebra_of_isClosedImmersion_pullback_map_of_quasiCompact
- Nyll.AlgebraicCurves.Geometry.Schemes.IsFinite_ringKrullDim_stalk_quotient_eq_zero
- Nyll.AlgebraicCurves.Geometry.Schemes.IsIrreducible_topologicalKrullDim_add_one_le_of_isClosed_of_ne
- Nyll.AlgebraicCurves.Geometry.Schemes.IsOpenImmersion_ringKrullDim_stalk_eq
- Nyll.AlgebraicCurves.Geometry.Schemes.IsProper_exists_fg_subalgebra_of_isProper_pullback_snd
- Nyll.AlgebraicCurves.Geometry.Schemes.IsPullback_exists_iso_Spec_quotient_comp_morphismRestrict_eq
- Nyll.AlgebraicCurves.Geometry.Schemes.IsPullback_surjective_app_and_ker_app_eq_map_ker_of_isAffineOpen
- Nyll.AlgebraicCurves.Geometry.Schemes.IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd
- Nyll.AlgebraicCurves.Geometry.Schemes.IsSeparated_of_comp_of_universallyClosed_of_surjective
- Nyll.AlgebraicCurves.Geometry.Schemes.IsZariskiLocalAtTarget_sigmaMap
- Nyll.AlgebraicCurves.Geometry.Schemes.LocallyOfFiniteType_of_comp_of_isFinite_of_flat_of_surjective
- Nyll.AlgebraicCurves.Geometry.Schemes.LocallyQuasiFinite_descendsAlong_surjective_inf_flat_inf_quasiCompact
- Nyll.AlgebraicCurves.Geometry.Schemes.LocallyQuasiFinite_of_flat_of_locallyQuasiFinite_genericFiber
- Nyll.AlgebraicCurves.Geometry.Schemes.LocallyQuasiFinite_ringKrullDim_stalk_quotient_eq_zero
- Nyll.AlgebraicCurves.Geometry.Schemes.SchemeHomOver_ext_of_forall_algebraicClosure_point_of_isReduced_of_flat
- Nyll.AlgebraicCurves.Geometry.Schemes.SchemeHomOver_isClosedImmersion_of_iff_exists_comp_eq_of_injective
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_app_injective_and_exists_of_forall_isAffineOpen
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_bijective_app_of_isPullback_of_bijective_of_isAffineOpen
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_exists_isClosed_irreducible_subset_fiber_of_not_quasiFiniteAt
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_finrank_comp_of_finrank_eq_const
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_finrank_morphismRestrict_eq_finrank
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_finrank_pullbackMap_of_comp_eq
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_isFinite_and_finrank_subschemeIota_ker_pow_of_comp_eq_id
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_isInvertible_ker_of_comp_eq_id
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_isInvertible_ker_of_comp_eq_id_of_mem_opens
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_isIso_stalkMap_genericPoint_of_isReduced_of_forall_specializes_of_forall_exists_div
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_map_germ_ker_ideal_eq_ker_stalkMap
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_mem_smoothLocus_of_flat_of_smoothOfRelativeDimension_pullback_snd
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_natCard_le_finrank_of_isFinite
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_nonempty_pullback_ker_pow_invModule_iso_of_isIso
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_ord_eq_of_ker_pow_ideal_eq_span
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_quasiFiniteAt_of_isPullback_of_locallyQuasiFinite
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_smoothLocus_le_preimage_of_isPullback
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_stalkMap_genericPoint_surjective_of_forall_exists_div
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Opens_finite_preimage_singleton_toSpecPolynomial
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Opens_isProper_toSpecPolynomial_of_maximal
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Opens_range_algebraMap_functionField_eq_iInf
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_OrderedAffineCover_exists_forall_le_preimage_of_compactSpace
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_OrderedAffineCover_exists_refinement_preimage_preimage_of_isSeparated
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_OrderedAffineCover_exists_refinement_pullback_fst_snd_of_isSeparated
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_OrderedAffineCover_nonempty_of_compactSpace
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_PartialMap_mem_domain_toRationalMap_of_valuationRing_stalk
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Pullback_isAffineOpen_and_exists_algEquiv_tensor_sections_fst_preimage_inf_snd_preimage
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_RationalMap_exists_specializes_ringKrullDim_le_one_of_not_mem_domain
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_H1baseChangeMap_surjective_and_eq_iff_of_surjective
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_HomOver_exists_isFrameOn_pullback_of_map_eq_smul
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_bijective_algebraMap_sections_baseChange_of_isReduced
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_bijective_kerBaseChangeHom_and_surjective_unit_app_of_subsingleton_H1
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_exists_baseChangeIsos_structureSheaf
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_exists_ideal_pullback_cover_ringEquiv_quotient_appLE_of_squareZero
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_exists_isFrameOn_pullback_stage_of_map_eq_smul
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_exists_isPullback_snd_specMap_algebraOfHom
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_exists_linearEquiv_kaehlerSectionsH0_regularDifferentials_apply_eq_kaehlerToFunctionField
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_exists_linearEquiv_overlap_quotient_baseChange_of_lift_of_compat
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_H0
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_exists_sectionsOf_baseChange_equiv_of_locallyTrivial
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_exists_sectionsOf_overlap_linearEquiv_baseChange_of_isInvertible
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_exists_sectionsOf_pullback_stageHom_equiv_lineBundle_appLE
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_exists_sectionsOf_unit_equiv_structureSheafSections
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_exists_stage_baseChangeIsos_structureSheaf
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_exists_stage_sectionsOf_baseChange_equiv_of_locallyTrivial
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_finiteType_algebraOfHom
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_finite_H0_H1_structureSheaf
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_finrank_H0_sectionsOf_baseChange_eq_and_subsingleton_H1_iff
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_finrank_H0_unit_fibre_eq_one_of_bijective_sections
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_finrank_H1_sectionsOf_unit_eq_and_finrank_H0_eq_one
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_flat_sections_of_flat
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_isOpen_setOf_subsingleton_H1_fibre
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_kaehlerToFunctionField_mem_regularDifferentials
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_nonempty_iso_iff_exists_units_of_sectionsOf_equiv_lineBundle
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_nonempty_iso_pullback_baseChangeSnd_of_sectionsOf_lift_appLE_of_overlap_iso
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_nonempty_linearEquiv_H1_sectionsOf_of_isSeparated
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_subsingleton_H1_sectionsOf_of_forall_field
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_subsingleton_H1_sectionsOf_of_subsingleton_H1
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_toH0_bijective
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_bijective_algebraMap_sections_of_isProper_of_isIntegral
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_eq_of_forall_mem_valuationSubring_of_isSeparated
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_existsUnique_germToFunctionField_eq_of_iSup_eq
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_existsUnique_hom_sigma_of_disjoint_iSup_eq_top
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_existsUnique_section_algebraMap_germ_eq_of_forall_mem_range
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_affine_quotient_of_finiteLocallyFree_equivalenceRelation
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_algEquiv_tensor_sections_pullback_fst_preimage_of_isAffineOpen
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_app_eq_app_of_isCompact_of_isDirectLimit
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_app_eq_of_isCompact_of_isDirectLimit
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_eq_closedPoint_and_forall_mem_of_valuationSubring
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_forall_eq_appLE_of_forall_map_eq_of_bijective
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_fromSpecStalk_specializes_and_mem_iff_residue_eq_zero_and_eq_genericPoint_iff
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_iSup_preimage_eq_top_of_isDirectLimit
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_isAlgClosed_factor_residueField_of_range_subset_singleton
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_isOpenImmersion_of_functionField_iso
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_isOpenImmersion_presheaf_overTotal_of_isOpen_of_chart
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_iso_comp_eq_of_isOpenImmersion_of_isProper
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_normSections_mul_map_eq_norm_of_isFinite_of_isIntegrallyClosed
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_quotient_of_finiteLocallyFree_equivalenceRelation
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_quotient_of_forall_exists_quotient_restrict
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_specializes_isLocalization_atPrime_stalk
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_finite_setOf_forall_mem_iff_mul_mem_of_isClosed_of_compl_subset_of_isAffineOpen
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_forall_mem_iff_of_subset_union_preimage_or_disjoint
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_isAffineOpen_and_exists_linearEquiv_tensor_sections_of_isPullback
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_isNoetherianRing_stalk_quotient_map_maximalIdeal_of_locallyOfFiniteType
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_quotient_baseChange_of_finiteLocallyFree_of_isPullback
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_subset_basicOpen_or_disjoint_of_isProper_of_isIrreducible
- Nyll.AlgebraicCurves.Geometry.Schemes.SmoothOfRelativeDimension_isDiscreteValuationRing_stalk_of_isClosed
- Nyll.AlgebraicCurves.Geometry.Schemes.SmoothOfRelativeDimension_isDiscreteValuationRing_stalk_of_section
- Nyll.AlgebraicCurves.Geometry.Schemes.SmoothOfRelativeDimension_le_topologicalKrullDim
- Nyll.AlgebraicCurves.Geometry.Schemes.SmoothOfRelativeDimension_topologicalKrullDim_le
- Nyll.AlgebraicCurves.Geometry.Schemes.SmoothOfRelativeDimension_topologicalKrullDim_preimage_singleton_eq
- Nyll.AlgebraicCurves.Geometry.Schemes.Smooth_descendsAlong_surjective_inf_flat_inf_quasiCompact
- Nyll.AlgebraicCurves.Geometry.Schemes.Smooth_exists_comp_eq_id_and_specMap_comp_eq_of_henselianLocalRing
- Nyll.AlgebraicCurves.Geometry.Schemes.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd
- Nyll.AlgebraicCurves.Geometry.Schemes.Smooth_exists_isOpen_isIrreducible_nhd
- Nyll.AlgebraicCurves.Geometry.Schemes.Smooth_exists_smoothOfRelativeDimension_of_preconnectedSpace
- Nyll.AlgebraicCurves.Geometry.Schemes.Smooth_isDiscreteValuationRing_stalk_of_forall_specializes
- Nyll.AlgebraicCurves.Geometry.Schemes.Smooth_isDomain_and_isIntegrallyClosed_stalk_of_isDiscreteValuationRing
- Nyll.AlgebraicCurves.Geometry.Schemes.Smooth_isReduced_of_isReduced_of_isLocallyNoetherian
- Nyll.AlgebraicCurves.Geometry.Schemes.Smooth_isRegularLocalRing_stalk
- Nyll.AlgebraicCurves.Geometry.Schemes.UniversallyInjective_of_forall_isAlgClosed_points_eq
- Nyll.AlgebraicCurves.Geometry.Schemes.bijective_algebraMap_appTop_of_isProper_of_isIntegral
- Nyll.AlgebraicCurves.Geometry.Schemes.bijective_appTop_of_bijective_appTop_pullback_snd_of_faithfullyFlat
- Nyll.AlgebraicCurves.Geometry.Schemes.bijective_appTop_of_forall_isMaximal
- Nyll.AlgebraicCurves.Geometry.Schemes.bijective_appTop_of_isProper_of_flat_of_isAdicComplete
- Nyll.AlgebraicCurves.Geometry.Schemes.bijective_appTop_of_isProper_of_flat_of_isNoetherianRing_of_isLocalRing
- Nyll.AlgebraicCurves.Geometry.Schemes.bijective_appTop_of_isProper_of_flat_of_locallyOfFinitePresentation_of_isLocalRing
- Nyll.AlgebraicCurves.Geometry.Schemes.bijective_appTop_pullback_snd_of_bijective_appTop
- Nyll.AlgebraicCurves.Geometry.Schemes.bijective_appTop_pullback_snd_of_bijective_appTop_fiberToSpecResidueField
- Nyll.AlgebraicCurves.Geometry.Schemes.bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections
- Nyll.AlgebraicCurves.Geometry.Schemes.bijective_appTop_pullback_snd_residue_of_bijective_appTop_of_isReduced
- Nyll.AlgebraicCurves.Geometry.Schemes.bijective_app_of_bijective_appTop_morphismRestrict
- Nyll.AlgebraicCurves.Geometry.Schemes.bijective_app_of_forall_isAffineOpen
- Nyll.AlgebraicCurves.Geometry.Schemes.bijective_app_of_isProper_of_flat_of_forall_bijective_appTop_fiberToSpecResidueField
- Nyll.AlgebraicCurves.Geometry.Schemes.comp_section_comp_eq_of_isClosedMap_of_surjective_app
- Nyll.AlgebraicCurves.Geometry.Schemes.dense_setOf_exists_section_of_isAlgClosed
- Nyll.AlgebraicCurves.Geometry.Schemes.eq_of_comp_eq_of_residue_comp_eq_of_formallyUnramified
- Nyll.AlgebraicCurves.Geometry.Schemes.eq_of_section_of_base_closedPoint_eq_of_ker_stalkMap_le
- Nyll.AlgebraicCurves.Geometry.Schemes.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk
- Nyll.AlgebraicCurves.Geometry.Schemes.existsUnique_lift_fromNormalization_kummer_of_isAffineOpen
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_algEquiv_sections_pullback_fst_preimage_tensor_of_isAffineOpen
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_algHom_retraction_stalk_and_ker_le_span_sup_sq_of_section_of_smoothOfRelativeDimension_one
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_comp_eq_of_isOpenImmersion_of_isProper_of_isDiscreteValuationRing_stalk
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_cover_forall_geomFibreH0Finrank_tensorPow_eq_eval_of_isClosedImmersion_of_flat_of_locallyOfFinitePresentation
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_eq_pullback_snd_comp_of_isProper
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_eq_snd_comp_of_comp_eq_const_of_isProper
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_etale_nhd_section_of_smooth
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_etale_of_formallyUnramified_stalkMap
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_fg_subalgebra_hom_pullback_of_hom_pullback_of_locallyOfFinitePresentation
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_fg_subalgebra_isAffine_pullback_of_isAffine_pullback
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_fg_subalgebra_isProper_flat_isPullback_of_isProper_of_flat_of_locallyOfFinitePresentation
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_fg_subalgebra_isPullback_of_iSup_eq_top_of_locallyOfFinitePresentation
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_fg_subalgebra_isPullback_of_isAffine_of_locallyOfFinitePresentation
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_fg_subalgebra_isPullback_of_locallyOfFinitePresentation
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_fg_subalgebra_opens_preimage_eq_of_isCompact
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_fg_subalgebra_pullback_fst_comp_eq_of_locallyOfFiniteType
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_finset_forall_norm_appLE_sub_lt_imp_false_of_ne_of_isSeparated
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_finset_forall_pointEquiv_eq_coe_mem_ball_of_differentiableOn_appLE_of_isSeparated
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_forall_geomFibreH0Finrank_tensorPow_eq_hilbertFunctionOf_of_point_geomFibre
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_forall_geomFibreH0Finrank_tensorPow_eq_hilbertFunctionOf_of_point_geomFibre_of_hom
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_forall_specMap_base_mem_of_isDirectLimit
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_isAffineOpen_forall_mem_of_isAffineHom_proj
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_isAffineOpen_forall_mem_of_isImmersion_proj
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_isAffineOpen_le_inf_forall_mem_of_finset
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_isAffineOpen_opens_le_preimage_forall_mem_of_forall_finset
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_isClopen_preimage_eq_of_isProper_of_henselianLocalRing
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_isClosedImmersion_forall_factors_iff_of_idealCut
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_isClosedImmersion_locallyOfFinitePresentation_forall_factors_iff_of_fg_idealCut
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_isFinite_to_proj_of_completeOrthogonalIdempotents
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isIntegral
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_isProper_surjective_isOpenImmersion_comp_eq_of_isSeparated
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_isPullback_glue_of_isPullback_of_isOpenImmersion
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_isUnit_appTop_eq_of_bijective_of_surjective_of_ker_le_maximalIdeal
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_iso_pullback_residue_of_iso_pullback
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_ker_stalkMap_eq_span_and_maximalIdeal_eq_of_section_of_smoothOfRelativeDimension_one
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_opensRestrict_pullback_snd
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_mem_isClosed_singleton_ne_of_isIrreducible
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_opens_flat_morphismRestrict_and_finrank_eq_and_mem_of_ringKrullDim_le_one_of_isFinite
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_over_hom_base_closedPoint_eq_of_isClosed_singleton
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_pow_eq_of_section_fromNormalization_kummer
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_pt_sigma_nat_and_eq_comp_sigmaInj_of_forall_represents_hilbertPolynomial_eq
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_rationalPoint_enumeration_of_natCard_pullback_eq
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_representableBy_of_representableBy_restrict_finiteEtale
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_representableBy_of_representableBy_restrict_finiteEtale_of_forall_orbit
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_ringEquiv_stalk_pullback_localization_tensorProduct_stalk_of_germ_snd
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_ringHom_functionField_germ_eq_of_base_genericPoint_eq
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_root_fromNormalization_kummer_existsUnique_lift
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_section_comp_eq_of_smooth_of_henselianLocalRing
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_section_of_isFinite_of_etale_of_isProper_of_henselianLocalRing_of_isNoetherianRing
- Nyll.AlgebraicCurves.Geometry.Schemes.exists_sum_appLE_mul_appLE_ne_zero_and_forall_eq_zero_of_ne_of_isSeparated
- Nyll.AlgebraicCurves.Geometry.Schemes.ext_of_forall_comp_eq_of_isAlgClosed
- Nyll.AlgebraicCurves.Geometry.Schemes.finite_appTop_of_isProper_of_isNoetherianRing
- Nyll.AlgebraicCurves.Geometry.Schemes.finite_setOf_pullback_fst_eq_of_isClosed_singleton
- Nyll.AlgebraicCurves.Geometry.Schemes.finrank_sections_pushforward_thickening_and_injective_unit_app_iff
- Nyll.AlgebraicCurves.Geometry.Schemes.flat_and_finrank_eq_of_isFinite_of_surjective_of_ringKrullDim_le_one
- Nyll.AlgebraicCurves.Geometry.Schemes.flat_and_surjective_of_forall_exists_iso_morphismRestrict_eq_pullback_fst
- Nyll.AlgebraicCurves.Geometry.Schemes.flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo
- Nyll.AlgebraicCurves.Geometry.Schemes.genericPoint_mem_preimage_comp_pullback_fst_of_injective_algebraMap
- Nyll.AlgebraicCurves.Geometry.Schemes.germToFunctionField_trace_eq_traceFunAlong_germToFunctionField
- Nyll.AlgebraicCurves.Geometry.Schemes.isFinite_and_etale_fromNormalization_kummer_of_isIntegrallyClosed
- Nyll.AlgebraicCurves.Geometry.Schemes.isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk
- Nyll.AlgebraicCurves.Geometry.Schemes.isIntegral_of_smooth_of_preconnectedSpace
- Nyll.AlgebraicCurves.Geometry.Schemes.isIso_morphismRestrict_and_smoothOfRelativeDimension_one_of_coe_eq_compl_range_of_isClosedImmersion
- Nyll.AlgebraicCurves.Geometry.Schemes.isIso_of_isOpenImmersion_of_isClosedImmersion_of_section_of_isConnected_fibres
- Nyll.AlgebraicCurves.Geometry.Schemes.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocalRing
- Nyll.AlgebraicCurves.Geometry.Schemes.isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocallyNoetherian
- Nyll.AlgebraicCurves.Geometry.Schemes.isOpen_irreducibleComponent_of_isDomain_stalk
- Nyll.AlgebraicCurves.Geometry.Schemes.isPreconnected_preimage_closedPoint_of_isProper_of_bijective_appTop
- Nyll.AlgebraicCurves.Geometry.Schemes.isPullback_lift_fst_comp_fst_snd_comp_fst_prodStr
- Nyll.AlgebraicCurves.Geometry.Schemes.isPullback_pullbackMap_fst_comp_of_isPullback_of_isPullback
- Nyll.AlgebraicCurves.Geometry.Schemes.isPushout_appTop_pullback_fst_appTop_pullback_snd_of_flat
- Nyll.AlgebraicCurves.Geometry.Schemes.isReduced_of_etale
- Nyll.AlgebraicCurves.Geometry.Schemes.isReduced_of_smooth_of_field
- Nyll.AlgebraicCurves.Geometry.Schemes.isReduced_of_smooth_over_field
- Nyll.AlgebraicCurves.Geometry.Schemes.isReduced_pullback_residue_of_forall_isReduced_stalk_quotient
- Nyll.AlgebraicCurves.Geometry.Schemes.isSeparated_sigmaDesc_of_forall_isSeparated
- Nyll.AlgebraicCurves.Geometry.Schemes.jacobsonSpace_of_locallyOfFiniteType
- Nyll.AlgebraicCurves.Geometry.Schemes.locallyQuasiFinite_of_forall_locallyQuasiFinite_schemeFibreEndo
- Nyll.AlgebraicCurves.Geometry.Schemes.maximalIdeal_stalk_eq_span_stalkSpecializes_of_ker_stalkMap_eq_span
- Nyll.AlgebraicCurves.Geometry.Schemes.not_isAffine_of_isProper_of_smoothOfRelativeDimension_one
- Nyll.AlgebraicCurves.Geometry.Schemes.prodKerGraph_comap_mapOnProdOver
- Nyll.AlgebraicCurves.Geometry.Schemes.ringKrullDim_stalk_eq_of_isFinite_endomorphism
- Nyll.AlgebraicCurves.Geometry.Schemes.ringKrullDim_stalk_eq_of_locallyQuasiFinite_endomorphism
- Nyll.AlgebraicCurves.Geometry.Schemes.smoothOfRelativeDimension_of_irreducibleSpace
- Nyll.AlgebraicCurves.Geometry.Schemes.stalkMap_surjective_and_ker_stalkMap_eq_map_ker_of_isPullback_of_surjective
- Nyll.AlgebraicCurves.Geometry.Schemes.subsingleton_H1_and_finrank_H0_sectionsOf_tensor_invModule_pow_ker_of_isAlgEquivZero
- Nyll.AlgebraicCurves.Geometry.Schemes.surj_inj_isSeparated_pieces_sigmaDesc_of_forall_represents_hilbertPolynomial_eq_of_nat_of_eq_comp_sigmaInj
- Nyll.AlgebraicCurves.Geometry.Schemes.trace_eq_zero_of_finrank_eq_char_of_forall_isClosed_eq
- Nyll.AlgebraicCurves.Geometry.Schemes.valuationRing_stalk_of_smoothOfRelativeDimension_one
- Nyll.AlgebraicCurves.Geometry.Schemes.RegularLocalRingQuotientNonZeroDivisorAscent
- Nyll.AlgebraicCurves.Geometry.Schemes.RegularLocalRingRegularSequenceAscent
- Nyll.AlgebraicCurves.Geometry.Schemes.RationalLocalization
- Nyll.AlgebraicCurves.Geometry.Schemes.RigidifiedLineBundleOfInvertible
- Nyll.AlgebraicCurves.Geometry.Schemes.SchemeFibreEndo
- Nyll.AlgebraicCurves.Geometry.Schemes.SchemeHomOver
- Nyll.AlgebraicCurves.Geometry.Schemes.SchemeHomOverBaseChange
- Nyll.AlgebraicCurves.Geometry.Schemes.SmoothOfClosedPoints
- Nyll.AlgebraicCurves.Geometry.Schemes.SplitTorusMu
- Nyll.AlgebraicCurves.Geometry.Schemes.TwoAffineOpenCoverH1BaseChange
- Nyll.AlgebraicCurves.Geometry.Schemes.TwoAffineOpenCoverKaehler
- Nyll.AlgebraicCurves.Geometry.Schemes.TwoAffineOpenCoverPreimage
- Nyll.AlgebraicCurves.Geometry.Schemes.TwoAffineOpenCoverSectional
- Nyll.AlgebraicCurves.Geometry.Schemes.ValuativeCriterion
- Nyll.AlgebraicCurves.Geometry.Schemes.FiniteExtensionPoint
- Nyll.AlgebraicCurves.Geometry.Schemes.FunctionFieldConstantExtension
- Nyll.AlgebraicCurves.Geometry.Schemes.FunctionFieldConstantExtensionScalars
Imported by1
This module has no indexed declarations. Its imports and full source are available here.