NYLL
Module

eq_of_comp_eq_of_residue_comp_eq_of_formallyUnramified.lean

Nyll.AlgebraicCurves.Geometry.Schemes.eq_of_comp_eq_of_residue_comp_eq_of_formallyUnramified
1 declaration indexed from sourceView source ↗

Module documentation

eq of comp eq of residue comp eq of formally Unramified

Imports6
  • Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
  • Mathlib.AlgebraicGeometry.ResidueField
  • Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  • Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
  • Mathlib.Tactic.Convert
  • Mathlib.Tactic.TermCongr
Imported by1

Declarations

theorem

eq_of_comp_eq_of_residue_comp_eq_of_formallyUnramified

L33 ↗
AlgebraicGeometry.eq_of_comp_eq_of_residue_comp_eq_of_formallyUnramified
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace eq_of_comp_eq_of_residue_comp_eq_of_formallyUnramified
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
Lean source · statement
theorem _root_.AlgebraicGeometry.eq_of_comp_eq_of_residue_comp_eq_of_formallyUnramified
    {X Y : Scheme.{u}} (g : X ⟶ Y) [FormallyUnramified g] [LocallyOfFiniteType g]
    (A : Type u) [CommRing A] [IsLocalRing A]
    (u₁ u₂ : Spec (CommRingCat.of A) ⟶ X) (hg : u₁ ≫ g = u₂ ≫ g)
    (hres : Spec.map (CommRingCat.ofHom (IsLocalRing.residue A)) ≫ u₁ =
      Spec.map (CommRingCat.ofHom (IsLocalRing.residue A)) ≫ u₂) :
    u₁ = u₂

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.