Commit 2024-10-21 15:44 0cb54c9f

View on Github →

feat(AlgebraicGeometry): dominant morphisms of schemes (#17961)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

added theorem AlgebraicGeometry.topologically_isLocalAtTarget'

Modified Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean

added theorem AlgebraicGeometry.IsDominant.comp_iff

added theorem AlgebraicGeometry.IsDominant.of_comp

added theorem AlgebraicGeometry.Scheme.Hom.denseRange

added theorem AlgebraicGeometry.dominant_eq_topologically

Modified Mathlib/Topology/LocalAtTarget.lean

added theorem denseRange_iff_denseRange_of_iSup_eq_top