Module

bijective_appTop_pullback_snd_of_bijective_appTop_fiberToSpecResidueField.lean

Nyll.AlgebraicCurves.Geometry.Schemes.bijective_appTop_pullback_snd_of_bijective_appTop_fiberToSpecResidueField

6 declarations indexed from sourceView source ↗

Module documentation

bijective app Top pullback snd of bijective app Top fiber To Spec Residue Field

Imports5

Mathlib.AlgebraicGeometry.ResidueField
Mathlib.AlgebraicGeometry.Fiber
Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Nyll.AlgebraicCurves.Geometry.Schemes.bijective_appTop_pullback_snd_of_bijective_appTop

Imported by2

theorem

bijective_of_bijective_comp_iso

L34 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_pullback_snd_of_bijective_appTop_fiberToSpecResidueField.FibreIdentGC3.bijective_of_bijective_comp_iso

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_pullback_snd_of_bijective_appTop_fiberToSpecResidueField
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace FibreIdentGC3

Lean source · statement

theorem bijective_of_bijective_comp_iso {R S T : CommRingCat.{u}} (f : R ⟶ S) (g : S ⟶ T) [IsIso g]
    (h : Function.Bijective (f ≫ g)) : Function.Bijective f

theorem

bijective_of_iso_comp_bijective

L40 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_pullback_snd_of_bijective_appTop_fiberToSpecResidueField.FibreIdentGC3.bijective_of_iso_comp_bijective

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_pullback_snd_of_bijective_appTop_fiberToSpecResidueField
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace FibreIdentGC3

Lean source · statement

theorem bijective_of_iso_comp_bijective {R S T : CommRingCat.{u}} (f : R ⟶ S) (g : S ⟶ T) [IsIso f]
    (h : Function.Bijective (f ≫ g)) : Function.Bijective g

theorem

bijective_comp_of_bijective

L46 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_pullback_snd_of_bijective_appTop_fiberToSpecResidueField.FibreIdentGC3.bijective_comp_of_bijective

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_pullback_snd_of_bijective_appTop_fiberToSpecResidueField
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace FibreIdentGC3

Lean source · statement

theorem bijective_comp_of_bijective {R S T : CommRingCat.{u}} (f : R ⟶ S) (g : S ⟶ T) [IsIso g]
    (h : Function.Bijective f) : Function.Bijective (f ≫ g)

theorem

bijective_iso_comp_of_bijective

L51 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_pullback_snd_of_bijective_appTop_fiberToSpecResidueField.FibreIdentGC3.bijective_iso_comp_of_bijective

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_pullback_snd_of_bijective_appTop_fiberToSpecResidueField
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace FibreIdentGC3

Lean source · statement

theorem bijective_iso_comp_of_bijective {R S T : CommRingCat.{u}} (f : R ⟶ S) (g : S ⟶ T) [IsIso f]
    (h : Function.Bijective g) : Function.Bijective (f ≫ g)

theorem

bijective_appTop_of_iso_over

L56 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_pullback_snd_of_bijective_appTop_fiberToSpecResidueField.FibreIdentGC3.bijective_appTop_of_iso_over

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_pullback_snd_of_bijective_appTop_fiberToSpecResidueField
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace FibreIdentGC3

Lean source · statement

theorem bijective_appTop_of_iso_over {P P' S : Scheme.{u}} (e : P ≅ P') (s : P ⟶ S) (s' : P' ⟶ S)
    (he : e.hom ≫ s' = s) (h : Function.Bijective s'.appTop) : Function.Bijective s.appTop

theorem

bijective_appTop_pullback_snd_of_bijective_appTop_fiberToSpecResidueField

L64 ↗

AlgebraicGeometry.bijective_appTop_pullback_snd_of_bijective_appTop_fiberToSpecResidueField

Source context 5 commands

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

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

Lean source · statement

theorem
  _root_.AlgebraicGeometry.bijective_appTop_pullback_snd_of_bijective_appTop_fiberToSpecResidueField
    {X Y : Scheme.{u}} (q : X ⟶ Y) [QuasiCompact q] [QuasiSeparated q]
    {K : Type u} [Field K] (k : Spec (CommRingCat.of K) ⟶ Y)
    (h : Function.Bijective (q.fiberToSpecResidueField (k.base (IsLocalRing.closedPoint
      K))).appTop) :
    Function.Bijective (pullback.snd q k).appTop

Module documentation

bijective app Top pullback snd of bijective app Top fiber To Spec Residue Field

Declarations

bijective_of_bijective_comp_iso

bijective_of_iso_comp_bijective

bijective_comp_of_bijective

bijective_iso_comp_of_bijective

bijective_appTop_of_iso_over

bijective_appTop_pullback_snd_of_bijective_appTop_fiberToSpecResidueField