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'