Commit 2025-02-12 14:43 aee31c77

View on Github →

feat(AlgebraicGeometry): the kernel of a morphism (#21431)

Estimated changes

Modified Mathlib/AlgebraicGeometry/IdealSheaf.lean

added theorem AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp

added theorem AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply

added theorem AlgebraicGeometry.Scheme.Hom.iUnion_support_ker_openCover_map_comp

added def AlgebraicGeometry.Scheme.Hom.ker

added theorem AlgebraicGeometry.Scheme.Hom.ker_apply

added theorem AlgebraicGeometry.Scheme.Hom.le_ker_comp

added theorem AlgebraicGeometry.Scheme.Hom.range_subset_ker_support

added theorem AlgebraicGeometry.Scheme.Hom.support_ker

added theorem AlgebraicGeometry.Scheme.ker_eq_top_of_isEmpty

added theorem AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion

added theorem AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal

added theorem AlgebraicGeometry.Scheme.ker_of_isAffine

Modified Mathlib/AlgebraicGeometry/Limits.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

added theorem AlgebraicGeometry.IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback

Modified Mathlib/Topology/Sheaves/Sheaf.lean

added theorem TopCat.Presheaf.IsSheaf.section_ext