Module

Scheme_Hom_isInvertible_ker_of_comp_eq_id_of_mem_opens.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_isInvertible_ker_of_comp_eq_id_of_mem_opens

3 declarations indexed from sourceView source ↗

Module documentation

Scheme Hom is Invertible ker of comp eq id of mem opens

Imports8

Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.RingTheory.Spectrum.Prime.Topology
Nyll.AlgebraicCurves.RelativeDivisors.Cartier
Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_isInvertible_ker_of_comp_eq_id
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_of_comap_of_support_subset_range

Imported by3

theorem

ker_eq_comap_of_isPullback'

L65 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_isInvertible_ker_of_comp_eq_id_of_mem_opens.AlgebraicGeometry.Scheme.IdealSheafData.ker_eq_comap_of_isPullback'

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_isInvertible_ker_of_comp_eq_id_of_mem_opens
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open scoped _root_.AlgebraicGeometry.Scheme in
open scoped _root_.AlgebraicGeometry.Scheme.IdealSheafData in

Lean source · statement

theorem Scheme.IdealSheafData.ker_eq_comap_of_isPullback' {P X' Y Z : Scheme.{u}} {fst : P ⟶ X'}
  {snd : P ⟶ Y}
    {f : X' ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) [IsClosedImmersion g] : fst.ker =
      g.ker.comap f

theorem

isInvertible_ker_of_comp_eq_id_of_mem_opens_aux

L84 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_isInvertible_ker_of_comp_eq_id_of_mem_opens.AlgebraicGeometry.Scheme.Hom.isInvertible_ker_of_comp_eq_id_of_mem_opens_aux

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_isInvertible_ker_of_comp_eq_id_of_mem_opens
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open scoped _root_.AlgebraicGeometry.Scheme in
open scoped _root_.AlgebraicGeometry.Scheme.Hom in

Lean source · statement

theorem Scheme.Hom.isInvertible_ker_of_comp_eq_id_of_mem_opens_aux
    {O : Type u} [CommRing O] [IsLocalRing O] {Y : Scheme.{u}} (πY : Y ⟶ Spec (CommRingCat.of O))
      [IsSeparated πY]
    (W : Y.Opens) [SmoothOfRelativeDimension 1 (W.ι ≫ πY)]
    (σ : Spec (CommRingCat.of O) ⟶ Y) (hσ : σ ≫ πY = 𝟙 _) (hW : σ.base (IsLocalRing.closedPoint O)
      ∈ W) :
    σ.ker.IsInvertible

theorem

isInvertible_ker_of_comp_eq_id_of_mem_opens

L115 ↗

AlgebraicGeometry.Scheme.Hom.isInvertible_ker_of_comp_eq_id_of_mem_opens

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_isInvertible_ker_of_comp_eq_id_of_mem_opens
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Hom.isInvertible_ker_of_comp_eq_id_of_mem_opens
    {O : Type u} [CommRing O] [IsLocalRing O] {Y : Scheme.{u}} (πY : Y ⟶ Spec (CommRingCat.of O))
      [IsSeparated πY]
    (W : Y.Opens) [SmoothOfRelativeDimension 1 (W.ι ≫ πY)]
    (σ : Spec (CommRingCat.of O) ⟶ Y) (hσ : σ ≫ πY = 𝟙 _) (hW : σ.base (IsLocalRing.closedPoint O)
      ∈ W) :
    σ.ker.IsInvertible

Module documentation

Scheme Hom is Invertible ker of comp eq id of mem opens

Declarations

ker_eq_comap_of_isPullback'

isInvertible_ker_of_comp_eq_id_of_mem_opens_aux

isInvertible_ker_of_comp_eq_id_of_mem_opens