Structures · Geometry
AlgebraicGeometry.Flat
A morphism of schemes f : X ⟶ Y is flat if for each affine U ⊆ Y and
V ⊆ f ⁻¹' U, the induced map Γ(Y, U) ⟶ Γ(X, V) is flat. This is equivalent to
asking that all stalk maps are flat (see AlgebraicGeometry.Flat.iff_flat_stalkMap).
- Defined in
- Mathlib.AlgebraicGeometry.Morphisms.Flat
- Shape
- One type argument · adds flat_appLE
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Forgetful instances
Provided automatically by
Concrete types that are instances3
- CategoryTheory.Limits.pullback
- AlgebraicGeometry.Scheme.Opens.toScheme
- CategoryTheory.Limits.sigmaObj
How is a type an instance?
Loading the hierarchy index…
Assumed by52
- AlgebraicGeometry.Scheme.Hom.finrank_comp_left_of_isIso
- AlgebraicGeometry.Scheme.Hom.finrank_pullback_snd
- AlgebraicGeometry.Scheme.Hom.flat_appLE
- AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian
- AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat
- AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right
- AlgebraicGeometry.Flat.stalkMap
- AlgebraicGeometry.Scheme.Hom.one_le_finrank_map
- AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_right
- AlgebraicGeometry.Flat.isQuotientMap_of_surjective
- AlgebraicGeometry.Flat.flat_appLE
- AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left
- AlgebraicGeometry.Scheme.Hom.flat_appTop
- AlgebraicGeometry.Flat.isIso_of_surjective_of_mono
- AlgebraicGeometry.Flat.epi_of_flat_of_surjective
- AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_left
- AlgebraicGeometry.Scheme.Hom.finrank_of_isPullback
- AlgebraicGeometry.instFaithfulOverSchemePullbackOfSurjectiveOfFlatOfQuasiCompact
- AlgebraicGeometry.instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian
- AlgebraicGeometry.UniversallyOpen.of_flat
- AlgebraicGeometry.Flat.instDescScheme
- AlgebraicGeometry.Flat.flat_of_affine_subset
- AlgebraicGeometry.Scheme.Hom.singleton_mem_fppfPrecoverage
- AlgebraicGeometry.isRegularEpi_of_flat_of_surjective_of_isAffine
- AlgebraicGeometry.Scheme.instEffectiveEpiOfQuasiCompactOfSurjectiveOfFlat
- AlgebraicGeometry.IsSchemeTheoreticallyDominant.pullbackFst
- AlgebraicGeometry.Flat.generalizingMap
- AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_finite_irreducibleComponents
- AlgebraicGeometry.instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian
- AlgebraicGeometry.Scheme.Hom.isIso_iff_finrank_eq
- AlgebraicGeometry.IsSchemeTheoreticallyDominant.of_isPullback
- AlgebraicGeometry.isIso_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat
- AlgebraicGeometry.Flat.instSndScheme
- AlgebraicGeometry.IsSchemeTheoreticallyDominant.pullbackSnd
- AlgebraicGeometry.instFaithfulOverSchemePullbackOfSurjectiveOfFlatOfLocallyOfFinitePresentation
- AlgebraicGeometry.Flat.comp
- AlgebraicGeometry.Scheme.Hom.one_le_finrank_iff_surjective
- AlgebraicGeometry.Flat.instFstScheme
- AlgebraicGeometry.IsOpenImmersion.of_flat_of_mono
- AlgebraicGeometry.instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian_1
- AlgebraicGeometry.Smooth.of_smooth_fiberToSpecResidueField
- AlgebraicGeometry.effectiveEpi_base_of_flat
- AlgebraicGeometry.Scheme.Hom.isLocallyConstant_finrank
- AlgebraicGeometry.GeometricallyIntegral.isIntegral_of_isLocallyNoetherian
- AlgebraicGeometry.instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian_1
- AlgebraicGeometry.Flat.instResLE
- AlgebraicGeometry.Etale.of_formallyUnramified_of_flat
- AlgebraicGeometry.Flat.instMorphismRestrict
- AlgebraicGeometry.Scheme.Hom.finrank_pullback_fst
- AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat
Ancestors0
No ancestors.