All.lean
Nyll.AlgebraicCurves.RelativeDivisors.All
0 declarations indexed from sourceView source ↗
Imports64
- Nyll.AlgebraicCurves.RelativeDivisors.Cartier
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_IsUniversal_exists_isAffineOpen_of_finset
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_IsUniversal_exists_sumMap
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_IsUniversal_geometricallyConnected
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_IsUniversal_isProper
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_card_le_of_subset_support
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_comap_curveChange_ofPoint_comp_eq_and_isIso_pullbackModuleComparison_of_isIso_morphismRestrict
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_comap_curveChange_ofPoint_eq_top_and_isIso_pullbackModuleComparison_of_disjoint
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_I_eq_ker_lift_and_supportedIn_of_finite_etale
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_I_eq_mul
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_I_eq_of_isProper_of_support_finite
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_I_eq_prodKerGraph
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_I_eq_prodKerGraph_and_supportedIn
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_I_eq_prodKerGraph_of_isAlgClosed
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_I_eq_zeroSchemeIdeal
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_I_eq_zeroSchemeIdeal_and_supportedIn_of_support_subset_of_isOpenImmersion
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_I_eq_zeroSchemeIdeal_of_ne_zero_of_isProper
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_I_eq_zeroSchemeIdeal_of_supportedIn
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_comap_eq_of_supportedIn
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_isAffineOpen_of_finset_of_universal_supportedIn
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_isUniversal
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_isUniversal_of_isAffine
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_polarisation_pair_of_block
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_sameDivisorScheme
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_snd_apply_eq_and_notMem_support
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_split
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_supportedIn_I_eq_mul_of_supportedIn
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_supportedIn_comap_eq_of_isSeparated
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_supportedIn_of_forall_finset
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_supportedIn_universal_of_smooth_opens
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_isInvertible_I
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_isInvertible_I_of_supportedIn
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_isInvertible_rigidify_lineBundle_tensor_idealModule_and_nonempty_pullback_iso_of_supportedIn
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_isInvertible_twistModule_and_nonempty_pullback_iso
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_isInvertible_twistModule_and_nonempty_pullback_iso_of_supportedIn
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_isOpenImmersion_presheaf_supportedIn_incl
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_isRepresentable_supportedIn
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_isSheaf_functor
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_isUniversal_empty
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_locallyOfFiniteType_quasiCompact_isSeparated_of_universal_supportedIn
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_nonempty_lineBundle_pullbackAlong_iso_invModule_pow_ker_mul_pow_prod_ker
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_nonempty_pullback_lineBundle_pullbackAlong_iso_of_supportedIn
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_nonempty_pullback_ofPoint_lineBundle_iso_and_idealModule_iso_of_range_subset
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_nonempty_rigidify_lineBundle_tensor_idealModule_pullbackAlong_iso_pullback_of_supportedIn
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_nonempty_twistModule_pullbackAlong_iso_pullback
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_nonempty_twistModule_pullbackAlong_iso_pullback_of_supportedIn
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_pullbackAlong_injective
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_pullbackAlong_ofPoint
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_supportedIn_ofPoint
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_supportedIn_of_lineBundle_iso_of_forall_zeroScheme_supportedIn
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDivFunctor
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDivOfPoint
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDivRestrict
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDivSum
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDivSupportedIn
- Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDivTwist2
- Nyll.AlgebraicCurves.RelativeDivisors.UniversalData
- Nyll.AlgebraicCurves.RelativeDivisors.UniversalSumKernel
- Nyll.AlgebraicCurves.RelativeDivisors.LinearPencilDivisor
- Nyll.AlgebraicCurves.RelativeDivisors.LinearPencilSections
- Nyll.AlgebraicCurves.RelativeDivisors.ChangeBase
Imported by1
This module has no indexed declarations. Its imports and full source are available here.