All.lean
Nyll.AlgebraicCurves.Geometry.Sheaves.All
0 declarations indexed from sourceView source ↗
Imports306
- Nyll.AlgebraicCurves.Geometry.Sheaves.IdealSheafHom
- Nyll.AlgebraicCurves.Geometry.Sheaves.IdealSheafModule
- Nyll.AlgebraicCurves.Geometry.Sheaves.IdealSheafModuleMaps
- Nyll.AlgebraicCurves.Geometry.Sheaves.KaehlerModule
- Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesBaseChangeHom
- Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesDet
- Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesGlueOfCocycle
- Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesIhomSections
- Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesLocallyFreeOfRank
- Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesNormModule
- Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesProjectionMorphism
- Nyll.SchemeTheory.Modules.PullbackMonoidal
- Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesPullbackMonoidalV2
- Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesPushforwardRestrict
- Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesRigidify
- Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesSectionZeroScheme
- Nyll.SchemeTheory.Modules.TensorSections
- Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesSectionsTensorV2
- Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesTensorPow
- Nyll.SchemeTheory.Modules.TensorPowers
- Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesTildePullback
- Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesWedge
- Nyll.AlgebraicCurves.Geometry.Sheaves.IdealSheafData_flat_subschemeInclusion_comp_of_forall_mul_mem_of_isDiscreteValuationRing
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_comap_of_isOpenImmersion
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_epi_unit_app_tensor_invModule_pow_and_exists_shortExact
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_exists_divisor_range_invModule_eq_lSpaceOn
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_exists_divisor_range_module_eq_lSpaceOn
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_exists_shortExact_thickening_unit
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_exists_tensor_iso_mul_module
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_isFinite_and_finrank_mul_subscheme_comp_eq_add
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_isInvertible_invModule
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_isInvertible_module
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_isIso_pullbackModuleComparison
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_mul_left_cancel
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_nonempty_module_tensor_invModule_iso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_nonempty_mul_invModule_iso_tensor
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_nonempty_pullback_invModule_iso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_of_comap_of_support_subset_range
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_of_forall_comap_openCover
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_pow
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_zeroSchemeIdeal_invModuleSection
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_comap_injective_of_flat_of_surjective
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_comap_ker_subschemeIota_comp_mapOnProdOver_eq_and_saturated_of_isDiscreteValuationRing
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_comap_mul
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_comap_ofIdealTop
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_eq_of_forall_comap_openCover_eq
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_exists_comap_eq_of_openCover
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_exists_iso_subscheme_comap_of_support_subset_range
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_ideal_comap_of_le
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_isInvertible_of_isInvertible_comap
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_isReduced_subscheme_vanishingIdeal_and_le_ker
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_nonempty_invModule_prod_pow_iso_tensorUnit_of_prod_pow_eq_zeroSchemeIdeal
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_pullbackModuleComparison_locallySurjective
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_range_moduleIota_app_and_injective
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_FiniteBySections_isFinite_of_unit
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_FiniteBySections_of_finiteBySections_unit
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_FiniteBySections_of_isFinite
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_FiniteBySections_of_iso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_FiniteBySections_tensor
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_FiniteBySections_tensorPow
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_Hom_epi_iff_locallySurjective
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_Hom_isIso_of_forall_exists_isIso_pullback_map
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_Hom_isIso_of_isIso_app_of_iSup_eq_top
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_Hom_mono_iff_injective
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_dual_eq_of_ihomEval_eq
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_existsUnique_ihomEval_eq
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_exists_basis_smul_pushforward
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_exists_isFrameOn_normModule
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_exists_isUnit_map_eq_mul_of_iso_tensorUnit
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_exists_isUnit_smul_eq
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_nonempty_iso_of_map_eq_smul_of_map_eq_smul
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_of_iSup
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_pullbackLocalSection
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_tensorPowSection
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_tensorSections
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_bijective_lift_tensorSectionsBilin
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_bijective_lift_tensorSectionsBilin_monoidalV2
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_dual
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_dual_monoidalV2
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_dual_tensor
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_eq_of_forall_pullbackSection_eq
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_eq_zero_of_pullback_map_eq_zero_of_isReduced
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_existsUnique_app_eq_smul
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_basis_one
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_bijective_smul_of_le_preimage_basicOpen_of_forall_isMaximal
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_comp_whiskerLeft_moduleIota_eq_of_pullbackSection_ker_eq_zero
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_divisor_range_eq_lSpaceOn
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_dual_iso_module_zeroSchemeIdeal
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_functionField_presentation
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_ideal_forall_iff_locallyIsoOver_unit_of_flat_of_isProper
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_ideal_forall_locallyIsoOver_unit_iff_map_eq_bot
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_isAffineOpen_isFrameOn_preimage_of_isDirectLimit
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_isClosedImmersion_forall_iff_locallyIsoOver_of_flat_of_isProper
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_isClosedImmersion_forall_iff_locallyIsoOver_unit_of_flat_of_isProper
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_isFrameOn
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_iso_invModule_zeroSchemeIdeal
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_iso_toDescentData_of_isAffineHom_of_flat_of_surjective
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_iso_toDescentData_of_isAffine_of_isAffineHom_of_flat_of_surjective
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_mem_and_nonempty_pullback_preimage_iso_unit_of_isFinite
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_nonempty_pullback_baseChangeSnd_iso_unit_of_forall_point
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_nonempty_pullback_preimage_basicOpen_iso_unit_of_forall_sections_linearEquiv
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_nonempty_pullback_preimage_iso_tensorUnit_of_isFinite
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_ratio_section
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_sectionsOf_equiv_lineBundle_one_add_of_pullback_quotient_isNilpotent
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_tensor_inverse
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_genericPoint_notMem_support_zeroSchemeIdeal
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_ideal_zeroSchemeIdeal_eq_span_of_app_eq_smul
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_isFrameOn_app_of_disjoint_support_zeroSchemeIdeal
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_isIso_ev_app_and_isIso_curry_braiding_ev
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_isIso_ev_app_tensorUnit
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_isIso_of_locallySurjective
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_nonempty_iso_pullback_pullback_of_rigidify_iso_unit
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_nonempty_iso_tensorUnit_of_field
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_nonempty_iso_tensorUnit_of_isLocalRing
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_nonempty_iso_tensorUnit_of_section_ne_zero_of_dual_section_ne_zero
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_nonempty_iso_unit_of_pullback_squareZero
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_nonempty_pullback_rigidify_iso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_nonempty_rigidify_pullback_tensor_iso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_normModule
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_pullbackSection_eq_zero_iff_mem_support
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_pullback_dual
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_pullback_dual_monoidalV2
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_rigidify
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_tensor
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_tensorPow
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_tensorPow_monoidalV2
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_tensor_monoidalV2
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_toDescentData_map_bijective_of_isAffineHom_of_flat_of_surjective
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_zeroSchemeIdeal_eq_of_app_eq_smul
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsLocallyFreeOfRank_of_forall_exists_opens
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsLocallyFreeOfRank_of_iso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsLocallyFreeOfRank_pullback
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ProjPresentation_exists_finiteBySections_pullback_of_quasiFiniteAt
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ProjPresentation_exists_forall_le_forall_exists_notMem_support_zeroSchemeIdeal_tensor_tensorPow
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj_monoidalV2
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ProjPresentation_isFinite_toProj_of_finite_setOf_forall_pullbackSection_eq_zero_iff
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ProjPresentation_isFinite_toProj_of_forall_pullbackSection_eq_zero_iff
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ProjPresentation_locallyQuasiFinite_of_forall_exists_eq_sum_smul
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ProjPresentation_mem_preimage_basicOpen_iff
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ProjPresentation_subset_support_zeroSchemeIdeal_or_disjoint
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_baseChangeHom_comp_horizontal
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_baseChangeHom_comp_vertical
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_epi_sheafification_map_of_locallySurjective
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_epi_whiskerRight_wedgeVec_of_shortExact
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_existsUnique_iso_forall_pullback_mapIso_eq_of_iSup_eq_top
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_app_eq_of_exact_of_app_eq_zero
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_away_finiteBySections_tensorPow_of_forall_geometricFibre
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_baseChange_sections_linearEquiv_pushforward_tensorUnit_of_affineOpen_le
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_basicOpen_forall_exists_frame
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_basicOpen_forall_exists_frame_of_frame_pullback
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_basis_pullback_of_field_point
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_eq_mul_and_eq_add_ord_of_presentations
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_eq_sub_of_cocycle_of_isAffineOpen
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_eq_sum_smul_pullbackSection_of_isReduced_of_finrank_eq
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_eq_sum_smul_pullbackSection_of_subsingleton_HSucc
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_fibreProduct_sections_bijective
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_finiteBySections_tensorPow_of_forall_geometricFibre
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_forall_eq_mul_of_presentations
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_forall_subsingleton_HSucc_tensorPow_of_isFinite_toProj
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_glueOfCocycle_mul_iso_tensor
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_glueOfCocycle_trivial_iso_tensorUnit
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_glueOfCocycle_twist_iso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_hom_tensorPow_three_support_zeroSchemeIdeal_eq
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_inter_iInter_support_zeroSchemeIdeal_eq_empty_of_topologicalKrullDim_lt
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_isFrameOn_normModule_and_app_eq_norm_smul
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_isFrameOn_normModule_forall_map_eq_norm_smul_of_isFrameOn_preimage
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_isFrameOn_normModule_map_eq_norm_smul_of_isFrameOn_preimage
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_isFrameOn_of_isUnit
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_isFrameOn_tensorPow_three_of_forall_nonempty_pullback_tensor_iso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_isInvertible_hom_ne_zero_finite_setOf_stabilizer
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_isInvertible_nonempty_pullback_iso_of_isInvertible_of_isDirectLimit
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_isInvertible_normModule_pullback_pullback_iso_pullback
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_isInvertible_pullbackSection_eq_zero_iff_notMem_of_isAffineOpen
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_isInvertible_pullback_curveChange_iso_of_closedCover
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_isInvertible_pullback_map_iso_unit_nonempty_pullback_iso_of_isDirectLimit
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_iso_app_eq_of_iSup_eq_top_of_forall_smul_eq
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_iso_app_eq_of_isFrameOn_of_eq_smul
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_iso_glueOfCocycle_app_eq_glueFrame
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_iso_pullback_of_isPullback
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_linearEquiv_sections_baseChange_of_locallyTrivial
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_linearEquiv_sections_pullback_of_isClosedImmersion_of_locallyTrivial
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_nonempty_iso_pullback_of_nonempty_iso_pullback_of_isDirectLimit
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_pullback_glueOfCocycle_iso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_refinement_isFrameOn_normModule_map_eq_normFun_smul
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_shortExact_ker_module_tensor_of_isClosedImmersion
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_twoTermComplex_sectionsEquiv_forall_baseChange
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_unitCocycle_map_eq_smul_of_isFrameOn
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exteriorPower_map_app_unit_iotaMulti_eq_det_smul
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_finite_sections_of_locallyTrivial
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_finrank_baseChange_sections_eq_one_of_locallyTrivial
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_forall_exists_basis_map_eq_of_forall_isAffineOpen
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_geomFibreH0Finrank_id_eq_finrank_sections
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_hom_ext_of_isIso_fromTildeGamma
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isClosed_setOf_le_finrank_sections_pullback_residueField
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isFrameOn_sheafificationAdjunction_unit_iotaMulti
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isInvertible_det_of_isLocallyFreeOfRank
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isInvertible_glueOfCocycle
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isInvertible_of_forall_exists_isFrameOn
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_baseChangeHom_iff_of_isPullback
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_baseChangeHom_of_forall_exists_isPullback
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_baseChangeHom_of_isOpenImmersion
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_baseChangeHom_of_twoAffineOpenCover
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_fromTildeGamma_iff_isLocalizedModule
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_fromTildeGamma_of_isLocalization_basicOpen
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_fromTildeGamma_of_locallyTrivial
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_of_isFrameOn_of_iSup_eq_top
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_projectionMorphism_of_iso_free
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_pullback_map_projectionMorphism_iff
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isLocalization_basicOpen_of_locallyTrivial_of_qcqs
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isLocallyFreeOfRank_one_iff_isInvertible
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isLocallyFreeOfRank_pushforward_of_forall_exists_isPullback
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isLocallyFreeOfRank_pushforward_of_twoAffineOpenCover
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isLocallyFreeOfRank_tilde
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isPrincipal_sub_single_of_presentation_ker_pow
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isPrincipal_sub_sub_of_presentations_tensor
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isStackFor_openCover
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isZero_exteriorPower_of_isLocallyFreeOfRank
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isZero_of_forall_exists_isZero_pullback_obj
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_leftUnitor_hom_app_tensorSections
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_det_succ_iso_det_tensor_of_shortExact
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_exteriorPower_free_iso_unit
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_iso_unit_of_forall_pullback_rigSection_iso_unit
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_normModule_invModule_ker_iso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_normModule_pullback_iso_tensorPow
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_normModule_tensor_iso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_normModule_unit_iso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_pullback_det_iso_det_pullback
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_pullback_exteriorPower_iso_exteriorPower_pullback
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_pullback_foldr_twist_iso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_pullback_fst_rigidify_iso_of_isInvertible
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_pullback_iso_of_bijective_app_of_le_opensRange
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_pullback_normModule_iso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_pullback_preimage_iso_unit_of_pullback_iso_unit
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_pullback_tensorPow_iso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_pullback_tensor_invModule_pow_tensor_module_iso_of_forall_notMem_support
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_pullback_tensor_pullback_iso_of_trivial_on_open
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_pushforward_hom_comp_iso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_pushforward_unit_tensor_iso_pushforward_pullback_of_isClosedImmersion
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_rigidify_iso_of_nonempty_pullback_iso_unit
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_tensorPow_mul_iso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ofUnitSection_sectionDual_app
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_projectionMorphism_naturality
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_pullbackComp_hom_app_comp_pullbackUnitIso_hom
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_pullbackComp_pullbackCongr_pasteSquares_app
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_pullbackTensorObjIso_hom_app_pullbackLocalSection
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_pullbackTensorUnitObjIso_hom_app_pullbackLocalSection_unitSection
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_pullbackUnitIso_conj_app_top_one_eq_appTop
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_pullbackUnitIso_hom_app_pullbackLocalSection_toUnitSection
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_pullback_locally_mem_span_unit
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_pullback_map_projectionMorphism_comp_counit
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_rankAtStalk_sections_eq_one_of_locallyTrivial
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_sheafificationAdjunction_unit_iotaMulti_eq_det_smul_of_eq_sum_smul
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_shortExact_map_pushforward_of_forall_exists_surjective_app
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_shortExact_of_app_injective_of_locallySurjective_of_locallyExact
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_surjective_app_of_shortExact_of_locallyTrivial
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_surjective_app_sup_of_shortExact_of_locallyTrivial
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_tensorPowSection_smul
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_tensorPowSection_smul_monoidalV2
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_toDescentData_essSurj_of_openCover
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_toDescentData_map_bijective_of_openCover
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_toDescentData_map_bijective_unit_of_flat_of_surjective
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_unitAutSection_comap_refinement_eq_appLE
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_unitAutSection_pullbackUnitIso_conj_opensI_eq_app_one
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_unitAutSection_trans_and_unitAutSection_refl
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_whiskerLeft_app_tensorSections
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_whiskerRight_app_tensorSections
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_zeroSchemeIdeal_comp_eq_of_isIso
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_zeroSchemeIdeal_comp_le
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_zeroSchemeIdeal_eq_ofIdealTop_of_app_eq_smul
- Nyll.AlgebraicCurves.Geometry.Sheaves.tilde_pullbackSpecIso_hom_app_top_unit_toOpen
- Nyll.AlgebraicCurves.Geometry.Sheaves.tilde_pullbackSpecIso_unit
- Nyll.AlgebraicCurves.Geometry.Sheaves.tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom
- Nyll.AlgebraicCurves.Geometry.Sheaves.RelativeSectionTwist
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_canonical_pullback_leg_relation
Imported by1
This module has no indexed declarations. Its imports and full source are available here.