Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-11 11:13 90ba0541

View on Github →

feat(algebraic_geometry): Define the category of AffineSchemes (#11326)

Estimated changes

Created src/algebraic_geometry/AffineScheme.lean

added def algebraic_geometry.AffineScheme.Spec

added def algebraic_geometry.AffineScheme.equiv_CommRing

added def algebraic_geometry.AffineScheme.forget_to_Scheme

added def algebraic_geometry.AffineScheme.Γ

added def algebraic_geometry.AffineScheme

added def algebraic_geometry.Scheme.iso_Spec

added theorem algebraic_geometry.is_affine_of_iso

added def algebraic_geometry.is_affine_open

added theorem algebraic_geometry.is_basis_affine_open

added theorem algebraic_geometry.mem_AffineScheme

added theorem algebraic_geometry.range_is_affine_open_of_open_immersion

added theorem algebraic_geometry.top_is_affine_open

Modified src/algebraic_geometry/Gamma_Spec_adjunction.lean

Modified src/algebraic_geometry/open_immersion.lean

added def algebraic_geometry.Scheme.of_restrict

added def algebraic_geometry.Scheme.restrict

added def algebraic_geometry.is_open_immersion.iso_of_range_eq

added def algebraic_geometry.is_open_immersion.iso_restrict

added def algebraic_geometry.is_open_immersion.lift

added theorem algebraic_geometry.is_open_immersion.lift_fac

added theorem algebraic_geometry.is_open_immersion.lift_uniq

Modified src/category_theory/adjunction/reflective.lean

added def category_theory.equiv_ess_image_of_reflective