EffectiveEpi

📁 Source: Mathlib/AlgebraicGeometry/EffectiveEpi.lean

Statistics

Metric	Count
Definitions	0
Theorems effectiveEpi_base_of_flat, isRegularEpi_of_flat_of_surjective_of_isAffine	2
Total	2

AlgebraicGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
effectiveEpi_base_of_flat 📖	mathematical	—	CategoryTheory.EffectiveEpi TopCat TopCat.instCategory PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom'	—	TopCat.effectiveEpi_iff_isQuotientMap Flat.isQuotientMap_of_surjective
isRegularEpi_of_flat_of_surjective_of_isAffine 📖	mathematical	—	CategoryTheory.IsRegularEpi Scheme Scheme.instCategory	—	Flat.epi_of_flat_of_surjective CategoryTheory.IsRegularEpi.of_epi_of_exists Scheme.Pullback.instHasPullback Flat.instSndScheme Surjective.instSndScheme IsOpenImmersion.hasPullback_of_right Scheme.instIsOpenImmersionF CategoryTheory.cancel_epi CategoryTheory.Limits.pullback.condition CategoryTheory.epi_of_effectiveEpi CategoryTheory.IsSplitEpi.EffectiveEpi CategoryTheory.IsSplitEpi.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Category.comp_id CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_snd_snd CategoryTheory.Category.assoc CategoryTheory.Limits.pullback.condition_assoc CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst_assoc Scheme.Cover.hom_ext Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange Scheme.instIsJointlySurjectivePreservingIsOpenImmersion isOpenImmersion_stableUnderBaseChange Scheme.Cover.ι_glueMorphisms

---

← Back to Index