FlatMono

📁 Source: Mathlib/AlgebraicGeometry/Morphisms/FlatMono.lean

Statistics

Metric	Count
Definitions	0
Theorems isIso_of_surjective_of_mono, of_flat_of_mono	2
Total	2

AlgebraicGeometry.Flat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_of_surjective_of_mono 📖	mathematical	—	CategoryTheory.IsIso AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory	—	CategoryTheory.MorphismProperty.of_pullback_fst_of_descendsAlong AlgebraicGeometry.descendsAlong_isomorphisms_surjective_inf_flat_inf_quasicompact AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.isIso_fst_of_mono

AlgebraicGeometry.IsOpenImmersion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_flat_of_mono 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion	—	AlgebraicGeometry.Scheme.Hom.continuous AlgebraicGeometry.Scheme.Hom.isOpenMap AlgebraicGeometry.UniversallyOpen.of_flat AlgebraicGeometry.Scheme.Hom.injective AlgebraicGeometry.instUniversallyInjectiveOfMonoScheme AlgebraicGeometry.Scheme.Hom.surjective Homeomorph.isCompact_preimage AlgebraicGeometry.Flat.isIso_of_surjective_of_mono of_isIso IsOpenMap.isOpen_range AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι AlgebraicGeometry.Scheme.Opens.range_ι Set.instReflSubset lift_fac CategoryTheory.MorphismProperty.of_postcomp AlgebraicGeometry.instHasOfPostcompPropertySchemeIsOpenImmersionOfIsStableUnderBaseChange AlgebraicGeometry.Flat.isStableUnderBaseChange AlgebraicGeometry.locallyOfFinitePresentation_isStableUnderBaseChange CategoryTheory.mono_of_mono_fac mono comp

---

← Back to Index