Module

IsIrreducible_topologicalKrullDim_add_one_le_of_isClosed_of_ne.lean

Nyll.AlgebraicCurves.Geometry.Schemes.IsIrreducible_topologicalKrullDim_add_one_le_of_isClosed_of_ne

7 declarations indexed from sourceView source ↗

Module documentation

Is Irreducible topological Krull Dim add one le of is Closed of ne

Imports1

Mathlib.Topology.KrullDimension

Imported by5

def

topIC

L33 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.IsIrreducible_topologicalKrullDim_add_one_le_of_isClosed_of_ne.P2mDim.topIC

Documentation

The whole irreducible subspace as an irreducible closed subset of itself.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsIrreducible_topologicalKrullDim_add_one_le_of_isClosed_of_ne
open Set Order TopologicalSpace Topology
universe u
namespace P2mDim
variable {X : Type u} [TopologicalSpace X] {Y Z : Set X}

Lean source · full declaration

def topIC (hZ : IsIrreducible Z) : IrreducibleCloseds Z where
  carrier := univ
  isIrreducible' := by
    have : IrreducibleSpace Z := Subtype.irreducibleSpace hZ
    exact IrreducibleSpace.isIrreducible_univ Z
  isClosed' := isClosed_univ

def

push

L41 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.IsIrreducible_topologicalKrullDim_add_one_le_of_isClosed_of_ne.P2mDim.push

Documentation

The map on irreducible closed subsets induced by inclusion of the underlying subspaces.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsIrreducible_topologicalKrullDim_add_one_le_of_isClosed_of_ne
open Set Order TopologicalSpace Topology
universe u
namespace P2mDim
variable {X : Type u} [TopologicalSpace X] {Y Z : Set X}

Lean source · statement

def push (hYZ : Y ⊆ Z) : IrreducibleCloseds Y → IrreducibleCloseds Z

theorem

push_strictMono

L44 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.IsIrreducible_topologicalKrullDim_add_one_le_of_isClosed_of_ne.P2mDim.push_strictMono

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsIrreducible_topologicalKrullDim_add_one_le_of_isClosed_of_ne
open Set Order TopologicalSpace Topology
universe u
namespace P2mDim
variable {X : Type u} [TopologicalSpace X] {Y Z : Set X}

Lean source · statement

theorem push_strictMono (hYZ : Y ⊆ Z) : StrictMono (push (X := X) hYZ)

theorem

coe_push_subset

L47 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.IsIrreducible_topologicalKrullDim_add_one_le_of_isClosed_of_ne.P2mDim.coe_push_subset

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsIrreducible_topologicalKrullDim_add_one_le_of_isClosed_of_ne
open Set Order TopologicalSpace Topology
universe u
namespace P2mDim
variable {X : Type u} [TopologicalSpace X] {Y Z : Set X}

Lean source · statement

theorem coe_push_subset (hYZ : Y ⊆ Z) (hY : IsClosed Y) (s : IrreducibleCloseds Y) :
    ((push hYZ s : IrreducibleCloseds Z) : Set Z) ⊆ (Subtype.val ⁻¹' Y : Set Z)

theorem

push_lt_top

L54 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.IsIrreducible_topologicalKrullDim_add_one_le_of_isClosed_of_ne.P2mDim.push_lt_top

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsIrreducible_topologicalKrullDim_add_one_le_of_isClosed_of_ne
open Set Order TopologicalSpace Topology
universe u
namespace P2mDim
variable {X : Type u} [TopologicalSpace X] {Y Z : Set X}

Lean source · statement

theorem push_lt_top (hZ : IsIrreducible Z) (hYZ : Y ⊆ Z) (hY : IsClosed Y) (hne : Y ≠ Z)
    (s : IrreducibleCloseds Y) : push hYZ s < topIC hZ

theorem

main

L62 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.IsIrreducible_topologicalKrullDim_add_one_le_of_isClosed_of_ne.P2mDim.main

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsIrreducible_topologicalKrullDim_add_one_le_of_isClosed_of_ne
open Set Order TopologicalSpace Topology
universe u
namespace P2mDim
variable {X : Type u} [TopologicalSpace X] {Y Z : Set X}

Lean source · statement

theorem main (hZ : IsIrreducible Z) (hY : IsClosed Y) (hYZ : Y ⊆ Z) (hne : Y ≠ Z) :
    topologicalKrullDim Y + 1 ≤ topologicalKrullDim Z

theorem

topologicalKrullDim_add_one_le_of_isClosed_of_ne

L83 ↗

IsIrreducible.topologicalKrullDim_add_one_le_of_isClosed_of_ne

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsIrreducible_topologicalKrullDim_add_one_le_of_isClosed_of_ne
open Set Order TopologicalSpace Topology
universe u

Lean source · statement

theorem _root_.IsIrreducible.topologicalKrullDim_add_one_le_of_isClosed_of_ne
    {X : Type u} [TopologicalSpace X] {Y Z : Set X}
    (hZ : IsIrreducible Z) (hY : IsClosed Y) (hYZ : Y ⊆ Z) (hne : Y ≠ Z) :
    topologicalKrullDim Y + 1 ≤ topologicalKrullDim Z

Module documentation

Is Irreducible topological Krull Dim add one le of is Closed of ne

Declarations

topIC

push

push_strictMono

coe_push_subset

push_lt_top

main

topologicalKrullDim_add_one_le_of_isClosed_of_ne