Commit 2024-07-21 21:46 f4aaf1c0

View on Github →

refactor(AlgebraicGeometry): Promote invApp to an iso. (#14868)

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

added theorem AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq

deleted theorem AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq

added def AlgebraicGeometry.Scheme.Hom.appIso

added theorem AlgebraicGeometry.Scheme.Hom.appIso_hom'

added theorem AlgebraicGeometry.Scheme.Hom.appIso_hom

added theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_app

added theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_appLE

added theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality

added theorem AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv

deleted theorem AlgebraicGeometry.Scheme.Hom.appLE_invApp

added theorem AlgebraicGeometry.Scheme.Hom.app_appIso_inv

deleted theorem AlgebraicGeometry.Scheme.Hom.app_invApp

deleted def AlgebraicGeometry.Scheme.Hom.invApp

deleted theorem AlgebraicGeometry.Scheme.Hom.invApp_app

deleted theorem AlgebraicGeometry.Scheme.Hom.invApp_naturality

deleted theorem AlgebraicGeometry.Scheme.Hom.inv_invApp

added theorem AlgebraicGeometry.Scheme.ofRestrict_appIso