Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-06-22 15:02
cc927b7a
View on Github →
feat: port AlgebraicGeometry.GammaSpecAdjunction (
#5079
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
added
theorem
AlgebraicGeometry.LocallyRingedSpace.comp_ring_hom_ext
added
theorem
AlgebraicGeometry.LocallyRingedSpace.isUnit_res_toΓSpecMapBasicOpen
added
theorem
AlgebraicGeometry.LocallyRingedSpace.not_mem_prime_iff_unit_in_stalk
added
theorem
AlgebraicGeometry.LocallyRingedSpace.toStalk_stalkMap_to_Γ_Spec
added
theorem
AlgebraicGeometry.LocallyRingedSpace.to_Γ_Spec_continuous
added
theorem
AlgebraicGeometry.LocallyRingedSpace.to_Γ_Spec_preim_basicOpen_eq
added
def
AlgebraicGeometry.LocallyRingedSpace.toΓSpec
added
def
AlgebraicGeometry.LocallyRingedSpace.toΓSpecBase
added
def
AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp
added
theorem
AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_iff
added
theorem
AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_spec
added
def
AlgebraicGeometry.LocallyRingedSpace.toΓSpecCBasicOpens
added
def
AlgebraicGeometry.LocallyRingedSpace.toΓSpecFun
added
theorem
AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq
added
def
AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace
added
theorem
AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq
added
theorem
AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec
added
def
AlgebraicGeometry.LocallyRingedSpace.ΓToStalk
added
theorem
AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle
added
def
AlgebraicGeometry.identityToΓSpec
added
def
AlgebraicGeometry.ΓSpec.adjunction
added
theorem
AlgebraicGeometry.ΓSpec.adjunction_counit_app
added
theorem
AlgebraicGeometry.ΓSpec.adjunction_homEquiv
added
theorem
AlgebraicGeometry.ΓSpec.adjunction_homEquiv_apply
added
theorem
AlgebraicGeometry.ΓSpec.adjunction_homEquiv_symm_apply
added
theorem
AlgebraicGeometry.ΓSpec.adjunction_unit_app
added
theorem
AlgebraicGeometry.ΓSpec.adjunction_unit_app_app_top
added
theorem
AlgebraicGeometry.ΓSpec.left_triangle
added
def
AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction
added
theorem
AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit
added
theorem
AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_unit
added
theorem
AlgebraicGeometry.ΓSpec.right_triangle
Modified
Mathlib/AlgebraicGeometry/LocallyRingedSpace.lean
added
theorem
AlgebraicGeometry.LocallyRingedSpace.Hom.ext'