Commit 2024-06-22 15:35 e4a15fb2

View on Github →

refactor(AlgebraicGeometry) Add notation Γ(X, U). (#14025)

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

modified theorem AlgebraicGeometry.IsAffineOpen.basicOpen_basicOpen_is_basicOpen

modified theorem AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff

modified theorem AlgebraicGeometry.IsAffineOpen.fromSpec_image_top

modified theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk'

added theorem AlgebraicGeometry.IsAffineOpen.opensRange_fromSpec

modified theorem AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff

modified theorem AlgebraicGeometry.IsAffineOpen.ιOpens_preimage

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

added theorem AlgebraicGeometry.ΓSpec.adjunction_counit_app'

added theorem AlgebraicGeometry.ΓSpec.adjunction_unit_app_Spec

added theorem AlgebraicGeometry.ΓSpec.adjunction_unit_map_basicOpen

added theorem AlgebraicGeometry.ΓSpec.toOpen_unit_app_val_c_app'

added theorem AlgebraicGeometry.ΓSpec.toOpen_unit_app_val_c_app

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

Modified Mathlib/AlgebraicGeometry/Properties.lean

modified theorem AlgebraicGeometry.eq_zero_of_basicOpen_eq_bot

modified theorem AlgebraicGeometry.isIntegral_of_isAffine_of_isDomain

modified theorem AlgebraicGeometry.isReduced_of_isAffine_isReduced

modified theorem AlgebraicGeometry.isReduced_of_isReduced_stalk

modified theorem AlgebraicGeometry.map_injective_of_isIntegral

modified theorem AlgebraicGeometry.reduce_to_affine_global

Modified Mathlib/AlgebraicGeometry/Restrict.lean

modified theorem AlgebraicGeometry.Scheme.map_basicOpen'

modified theorem AlgebraicGeometry.Scheme.map_basicOpen

modified theorem AlgebraicGeometry.Scheme.map_basicOpen_map

modified def AlgebraicGeometry.Scheme.restrictIsoOfEq

modified def AlgebraicGeometry.Scheme.restrictRestrict

modified def AlgebraicGeometry.Scheme.restrictRestrictComm

modified theorem AlgebraicGeometry.Scheme.restrictRestrict_hom_restrict

modified theorem AlgebraicGeometry.Scheme.restrictRestrict_inv_restrict_restrict

modified def AlgebraicGeometry.morphismRestrictRestrictBasicOpen

Modified Mathlib/AlgebraicGeometry/Scheme.lean

added theorem AlgebraicGeometry.Scheme.Spec_map_appLE

added theorem AlgebraicGeometry.Scheme.Spec_map_base

added theorem AlgebraicGeometry.Scheme.Spec_map_c_app

added theorem AlgebraicGeometry.Scheme.Spec_obj_carrier

added theorem AlgebraicGeometry.Scheme.Spec_obj_presheaf

added theorem AlgebraicGeometry.Scheme.Spec_obj_sheaf

added def AlgebraicGeometry.Scheme.SpecΓIdentity

modified def AlgebraicGeometry.Scheme.basicOpen

modified theorem AlgebraicGeometry.Scheme.basicOpen_of_isUnit

modified theorem AlgebraicGeometry.Scheme.basicOpen_restrict

modified theorem AlgebraicGeometry.Scheme.basicOpen_zero

added theorem AlgebraicGeometry.Scheme.eqToHom_c_app

modified theorem AlgebraicGeometry.Scheme.id_app

modified theorem AlgebraicGeometry.Scheme.inv_val_c_app

modified theorem AlgebraicGeometry.Scheme.mem_basicOpen_top'

modified theorem AlgebraicGeometry.Scheme.mem_basicOpen_top

modified theorem AlgebraicGeometry.Scheme.preimage_basicOpen

modified theorem AlgebraicGeometry.Scheme.Γ_obj_op

modified theorem AlgebraicGeometry.basicOpen_eq_of_affine'

Modified Mathlib/AlgebraicGeometry/Spec.lean

added def AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity

deleted def AlgebraicGeometry.SpecΓIdentity