structure BorelWeilData : Type (max (max (max (max (max (max (u + 1) (u_1 + 1)) (u_2 + 1)) (u_3 + 1)) (u_4 + 1)) (u_5 + 1)) (v + 1))

• k : Type u
• field_k : Field self.k
• 𝔤 : Type v
• lieRing : LieRing self.𝔤
• lieAlgebra : LieAlgebra self.k self.𝔤
• G : Type u_1
• group_G : Group self.G
• WeightLattice : Type u_2
• wl_addCommGroup : AddCommGroup self.WeightLattice
• IsDominant : self.WeightLattice → Prop
• IrrepModule : self.WeightLattice → Type u_3
• irrepAddCommGroup (w : self.WeightLattice) : AddCommGroup (self.IrrepModule w)
• irrepModule (w : self.WeightLattice) : Module self.k (self.IrrepModule w)
• irrepFinDim (w : self.WeightLattice) : Module.Finite self.k (self.IrrepModule w)
• irrepRep (w : self.WeightLattice) : Representation self.k self.G (self.IrrepModule w)
• FlagVar : Type u_4
• GlobalSections : self.WeightLattice → Type u_5
• sectionsAddCommGroup (w : self.WeightLattice) : AddCommGroup (self.GlobalSections w)
• sectionsModule (w : self.WeightLattice) : Module self.k (self.GlobalSections w)
• sectionsRep (w : self.WeightLattice) : Representation self.k self.G (self.GlobalSections w)

theorem borelWeil_Phi_equivariant (D : BorelWeilData) (μ : D.WeightLattice) (hμ : D.IsDominant μ) : ∃ (Ψ : D.GlobalSections μ ≃ₗ[D.k] Module.Dual D.k (D.IrrepModule μ)), ∀ (g : D.G), ↑Ψ ∘ₗ (D.sectionsRep μ) g = (D.irrepRep μ).dual g ∘ₗ ↑Ψ

theorem borelWeil_Phi_linearEquiv (D : BorelWeilData) (μ : D.WeightLattice) (hμ : D.IsDominant μ) : Nonempty (D.GlobalSections μ ≃ₗ[D.k] Module.Dual D.k (D.IrrepModule μ))

theorem borelWeil_dominant (D : BorelWeilData) (μ : D.WeightLattice) (hμ : D.IsDominant μ) : Nonempty ((D.sectionsRep μ).Equiv (D.irrepRep μ).dual)

theorem borelWeil_nonDominant (D : BorelWeilData) (μ : D.WeightLattice) (hμ : ¬D.IsDominant μ) : Subsingleton (D.GlobalSections μ)

theorem theorem_27_3 (D : BorelWeilData) (μ : D.WeightLattice) : (D.IsDominant μ → Nonempty ((D.sectionsRep μ).Equiv (D.irrepRep μ).dual)) ∧ (¬D.IsDominant μ → Subsingleton (D.GlobalSections μ))

structure ParabolicBorelWeilDataextends BorelWeilData : Type (max (max (max (max (max (max (max (max (max (u_1 + 1) (u_10 + 1)) (u_2 + 1)) (u_3 + 1)) (u_4 + 1)) (u_5 + 1)) (u_6 + 1)) (u_7 + 1)) (u_8 + 1)) (u_9 + 1))

• k : Type u_10
• field_k : Field self.k
• 𝔤 : Type u_9
• lieRing : LieRing self.𝔤
• lieAlgebra : LieAlgebra self.k self.𝔤
• G : Type u_8
• group_G : Group self.G
• WeightLattice : Type u_7
• wl_addCommGroup : AddCommGroup self.WeightLattice
• IsDominant : self.WeightLattice → Prop
• IrrepModule : self.WeightLattice → Type u_6
• irrepAddCommGroup (w : self.WeightLattice) : AddCommGroup (self.IrrepModule w)
• irrepModule (w : self.WeightLattice) : Module self.k (self.IrrepModule w)
• irrepFinDim (w : self.WeightLattice) : Module.Finite self.k (self.IrrepModule w)
• irrepRep (w : self.WeightLattice) : Representation self.k self.G (self.IrrepModule w)
• FlagVar : Type u_5
• GlobalSections : self.WeightLattice → Type u_4
• sectionsAddCommGroup (w : self.WeightLattice) : AddCommGroup (self.GlobalSections w)
• sectionsModule (w : self.WeightLattice) : Module self.k (self.GlobalSections w)
• sectionsRep (w : self.WeightLattice) : Representation self.k self.G (self.GlobalSections w)
• SimpleRoots : Type u_1
• S : Set self.SimpleRoots
• coroot_pairing : self.WeightLattice → self.SimpleRoots → ℤ
• PartialFlagVar : Type u_2
• projection : self.FlagVar → self.PartialFlagVar
• PartialFlagSections : self.WeightLattice → Type u_3
• pfSectionsAddCommGroup (w : self.WeightLattice) : AddCommGroup (self.PartialFlagSections w)
• pfSectionsModule (w : self.WeightLattice) : Module self.k (self.PartialFlagSections w)
• pfSectionsRep (w : self.WeightLattice) : Representation self.k self.G (self.PartialFlagSections w)

def ParabolicBorelWeilData.IsOrthogonalToS (D : ParabolicBorelWeilData) (μ : D.WeightLattice) : Prop

theorem sections_equiv_of_orthogonal (D : ParabolicBorelWeilData) (μ : D.WeightLattice) (hμ_orth : D.IsOrthogonalToS μ) : Nonempty ((D.pfSectionsRep μ).Equiv (D.sectionsRep μ))

theorem borelWeil_parabolic_dominant (D : ParabolicBorelWeilData) (μ : D.WeightLattice) (hμ_dom : D.IsDominant μ) (hμ_orth : D.IsOrthogonalToS μ) : Nonempty ((D.pfSectionsRep μ).Equiv (D.irrepRep μ).dual)

def nilpotentCone (k : Type u_1) (𝔤 : Type u_2) [CommRing k] [LieRing 𝔤] [LieAlgebra k 𝔤] : Set 𝔤

structure SpringerResolutionData : Type (max (max (max (u + 1) (u_1 + 1)) (u_2 + 1)) (v + 1))

• k : Type u
• field_k : Field self.k
• 𝔤 : Type v
• lieRing : LieRing self.𝔤
• lieAlgebra : LieAlgebra self.k self.𝔤
• FlagVar : Type u_1
• CotangentBundle : Type u_2
• springerMap : self.CotangentBundle → self.𝔤
• springerMap_mem_nilpotentCone (y : self.CotangentBundle) : self.springerMap y ∈ nilpotentCone self.k self.𝔤
• bundleProjection : self.CotangentBundle → self.FlagVar
• cotangentBundle_ext (y₁ y₂ : self.CotangentBundle) : self.bundleProjection y₁ = self.bundleProjection y₂ → self.springerMap y₁ = self.springerMap y₂ → y₁ = y₂
• IsRegularNilpotent : self.𝔤 → Prop
• regularNilpotent_mem (e : self.𝔤) : self.IsRegularNilpotent e → e ∈ nilpotentCone self.k self.𝔤
• regularNilpotent_nonempty : ∃ (e : self.𝔤), self.IsRegularNilpotent e
• isInBorel : self.𝔤 → self.FlagVar → Prop
• isInBorel_of_springerMap (y : self.CotangentBundle) : self.isInBorel (self.springerMap y) (self.bundleProjection y)
• rho_dual : self.𝔤

theorem rho_dual_pins_fiber_thm (D : SpringerResolutionData) (e : D.𝔤) : D.IsRegularNilpotent e → ⁅D.rho_dual, e⁆ = e ∧ ∃ (b₀ : D.FlagVar), ∀ (y : D.CotangentBundle), D.springerMap y = e → D.bundleProjection y = b₀

theorem SpringerResolutionData.rho_dual_pins_fiber (D : SpringerResolutionData) (e : D.𝔤) : D.IsRegularNilpotent e → ⁅D.rho_dual, e⁆ = e ∧ ∃ (b₀ : D.FlagVar), ∀ (y : D.CotangentBundle), D.springerMap y = e → D.bundleProjection y = b₀

def SpringerResolutionData.closedEmbedding (D : SpringerResolutionData) : D.CotangentBundle → D.FlagVar × D.𝔤

theorem SpringerResolutionData.closedEmbedding_eq (D : SpringerResolutionData) (y : D.CotangentBundle) : D.closedEmbedding y = (D.bundleProjection y, D.springerMap y)

theorem springerMap_surjective_onto_thm (D : SpringerResolutionData) (x : D.𝔤) : x ∈ nilpotentCone D.k D.𝔤 → ∃ (y : D.CotangentBundle), D.springerMap y = x

theorem SpringerResolutionData.springerMap_surjective (D : SpringerResolutionData) (x : D.𝔤) : x ∈ nilpotentCone D.k D.𝔤 → ∃ (y : D.CotangentBundle), D.springerMap y = x

theorem SpringerResolutionData.closedEmbedding_injective (D : SpringerResolutionData) : Function.Injective D.closedEmbedding

theorem SpringerResolutionData.rho_dual_grading_pins_fiber (D : SpringerResolutionData) (e : D.𝔤) (hreg : D.IsRegularNilpotent e) : ∃ (h : D.𝔤), ⁅h, e⁆ = e ∧ ∃ (b₀ : D.FlagVar), ∀ (y : D.CotangentBundle), D.springerMap y = e → D.bundleProjection y = b₀

theorem SpringerResolutionData.regularNilpotent_unique_fiber (D : SpringerResolutionData) (e : D.𝔤) (hreg : D.IsRegularNilpotent e) (y₁ y₂ : D.CotangentBundle) (h₁ : D.springerMap y₁ = e) (h₂ : D.springerMap y₂ = e) : D.bundleProjection y₁ = D.bundleProjection y₂

theorem SpringerResolutionData.springer_fiber_singleton (D : SpringerResolutionData) (e : D.𝔤) : D.IsRegularNilpotent e → ∃! y : D.CotangentBundle, D.springerMap y = e

noncomputable def SpringerResolutionData.mk' (k : Type u_1) [Field k] (𝔤 : Type u_2) [LieRing 𝔤] [LieAlgebra k 𝔤] (FlagVar : Type u_3) (CotangentBundle : Type u_4) (springerMap : CotangentBundle → 𝔤) (bundleProjection : CotangentBundle → FlagVar) (IsRegularNilpotent : 𝔤 → Prop) (hSpringerMap_mem : ∀ (y : CotangentBundle), springerMap y ∈ nilpotentCone k 𝔤) (hCotangentBundle_ext : ∀ (y₁ y₂ : CotangentBundle), bundleProjection y₁ = bundleProjection y₂ → springerMap y₁ = springerMap y₂ → y₁ = y₂) (hRegNilpMem : ∀ (e : 𝔤), IsRegularNilpotent e → e ∈ nilpotentCone k 𝔤) (hRegNilpNonempty : ∃ (e : 𝔤), IsRegularNilpotent e) (isInBorel : 𝔤 → FlagVar → Prop) (hIsInBorel_of_springerMap : ∀ (y : CotangentBundle), isInBorel (springerMap y) (bundleProjection y)) (rho_dual : 𝔤) : SpringerResolutionData

theorem regularNilpotent_unique_borel (D : SpringerResolutionData) (e : D.𝔤) (hreg : D.IsRegularNilpotent e) (y₁ y₂ : D.CotangentBundle) (h₁ : D.springerMap y₁ = e) (h₂ : D.springerMap y₂ = e) : D.bundleProjection y₁ = D.bundleProjection y₂

theorem springerMap_isResolution (D : SpringerResolutionData) : (∀ (e : D.𝔤), D.IsRegularNilpotent e → ∃! y : D.CotangentBundle, D.springerMap y = e) ∧ Function.Injective D.closedEmbedding ∧ ∀ x ∈ nilpotentCone D.k D.𝔤, ∃ (y : D.CotangentBundle), D.springerMap y = x

structure SkewSymmetricBilinearForm (k : Type u_1) (M : Type u_2) [CommRing k] [AddCommGroup M] [Module k M] : Type (max u_1 u_2)

• bilin : M →ₗ[k] M →ₗ[k] k
• skew_symm (x y : M) : (self.bilin x) y = -(self.bilin y) x

def SkewSymmetricBilinearForm.IsNondegenerate {k : Type u_1} {M : Type u_2} [CommRing k] [AddCommGroup M] [Module k M] (ω : SkewSymmetricBilinearForm k M) : Prop

def kirillovKostantForm (k : Type u_1) (𝔤 : Type u_2) [CommRing k] [LieRing 𝔤] [LieAlgebra k 𝔤] (f : 𝔤 →ₗ[k] k) : SkewSymmetricBilinearForm k 𝔤

def coadjointStabilizer (k : Type u_1) (𝔤 : Type u_2) [CommRing k] [LieRing 𝔤] [LieAlgebra k 𝔤] (f : 𝔤 →ₗ[k] k) : Submodule k 𝔤

theorem kirillovKostant_kernel (k : Type u_1) (𝔤 : Type u_2) [CommRing k] [LieRing 𝔤] [LieAlgebra k 𝔤] (f : 𝔤 →ₗ[k] k) (x : 𝔤) : (∀ (y : 𝔤), ((kirillovKostantForm k 𝔤 f).bilin x) y = 0) ↔ x ∈ coadjointStabilizer k 𝔤 f

theorem kirillovKostant_closed (k : Type u_1) (𝔤 : Type u_2) [CommRing k] [LieRing 𝔤] [LieAlgebra k 𝔤] (f : 𝔤 →ₗ[k] k) (x y z : 𝔤) : f ⁅y, ⁅x, z⁆⁆ + f ⁅z, ⁅y, x⁆⁆ + f ⁅x, ⁅z, y⁆⁆ = 0

structure CoadjointOrbitData (k : Type u_1) (𝔤 : Type u_2) [CommRing k] [LieRing 𝔤] [LieAlgebra k 𝔤] : Type (max (max u_1 u_2) (u_3 + 1))

• G : Type u_3
• instGroup : Group self.G
• Ad : self.G →* 𝔤 ≃ₗ[k] 𝔤
• Ad_preserves_bracket (g : self.G) (x y : 𝔤) : (self.Ad g) ⁅x, y⁆ = ⁅(self.Ad g) x, (self.Ad g) y⁆
• coadjointAction : self.G → (𝔤 →ₗ[k] k) → 𝔤 →ₗ[k] k
• coadjoint_formula (g : self.G) (f : 𝔤 →ₗ[k] k) (x : 𝔤) : (self.coadjointAction g f) x = f ((self.Ad g⁻¹) x)

def CoadjointOrbitData.orbit {k' : Type u_1} {𝔤' : Type u_2} [CommRing k'] [LieRing 𝔤'] [LieAlgebra k' 𝔤'] (data : CoadjointOrbitData k' 𝔤') (f : 𝔤' →ₗ[k'] k') : Set (𝔤' →ₗ[k'] k')

theorem CoadjointOrbitData.mem_orbit_iff {k' : Type u_1} {𝔤' : Type u_2} [CommRing k'] [LieRing 𝔤'] [LieAlgebra k' 𝔤'] (data : CoadjointOrbitData k' 𝔤') (f ξ : 𝔤' →ₗ[k'] k') : ξ ∈ data.orbit f ↔ ∃ (g : data.G), data.coadjointAction g f = ξ

theorem CoadjointOrbitData.Ad_inv_cancel_left {k' : Type u_1} {𝔤' : Type u_2} [CommRing k'] [LieRing 𝔤'] [LieAlgebra k' 𝔤'] (data : CoadjointOrbitData k' 𝔤') (g : data.G) (x : 𝔤') : (data.Ad g⁻¹) ((data.Ad g) x) = x

theorem kirillovKostant_G_invariant {k' : Type u_1} {𝔤' : Type u_2} [CommRing k'] [LieRing 𝔤'] [LieAlgebra k' 𝔤'] (data : CoadjointOrbitData k' 𝔤') (g : data.G) (f : 𝔤' →ₗ[k'] k') (y z : 𝔤') : (data.coadjointAction g f) ⁅(data.Ad g) y, (data.Ad g) z⁆ = f ⁅y, z⁆

theorem kirillovKostant_symplectic {k' : Type u_1} {𝔤' : Type u_2} [CommRing k'] [LieRing 𝔤'] [LieAlgebra k' 𝔤'] (data : CoadjointOrbitData k' 𝔤') (f : 𝔤' →ₗ[k'] k') : (∀ (y z : 𝔤'), f ⁅y, z⁆ = -f ⁅z, y⁆) ∧ (∀ (x : 𝔤'), (∀ (y : 𝔤'), f ⁅x, y⁆ = 0) ↔ x ∈ coadjointStabilizer k' 𝔤' f) ∧ (∀ (g : data.G) (y z : 𝔤'), (data.coadjointAction g f) ⁅(data.Ad g) y, (data.Ad g) z⁆ = f ⁅y, z⁆) ∧ ∀ (x y z : 𝔤'), f ⁅y, ⁅x, z⁆⁆ + f ⁅z, ⁅y, x⁆⁆ + f ⁅x, ⁅z, y⁆⁆ = 0

def nilpotentCone_singularLocus (k : Type u_3) (𝔤 : Type u_4) [CommRing k] [LieRing 𝔤] [LieAlgebra k 𝔤] [Module.Finite k 𝔤] [Module.Free k 𝔤] : Set 𝔤

structure NilpotentConeOrbitData (k : Type u_3) (𝔤 : Type u_4) [Field k] [LieRing 𝔤] [LieAlgebra k 𝔤] [Module.Finite k 𝔤] [Module.Free k 𝔤] [LieAlgebra.IsSemisimple k 𝔤] : Type u_4

• dimVariety : Set 𝔤 → ℕ
• dim_nilpCone_eq : self.dimVariety (nilpotentCone k 𝔤) = Module.finrank k 𝔤 - LieAlgebra.rank k 𝔤
• dim_nilpCone_even : Even (self.dimVariety (nilpotentCone k 𝔤))
• dim_singLocus_even : Even (self.dimVariety (nilpotentCone_singularLocus k 𝔤))
• dim_singLocus_lt : self.dimVariety (nilpotentCone_singularLocus k 𝔤) < self.dimVariety (nilpotentCone k 𝔤)

theorem semisimple_finrank_eq_rank_add_two_mul (k : Type u_3) (𝔤 : Type u_4) [Field k] [LieRing 𝔤] [LieAlgebra k 𝔤] [Module.Finite k 𝔤] [Module.Free k 𝔤] [LieAlgebra.IsSemisimple k 𝔤] : ∃ (n : ℕ), Module.finrank k 𝔤 = LieAlgebra.rank k 𝔤 + 2 * n

theorem nilpotentCone_dim_even (k : Type u_3) (𝔤 : Type u_4) [Field k] [LieRing 𝔤] [LieAlgebra k 𝔤] [Module.Finite k 𝔤] [Module.Free k 𝔤] [LieAlgebra.IsSemisimple k 𝔤] : Even (Module.finrank k 𝔤 - LieAlgebra.rank k 𝔤)

theorem nilpotentCone_singLocus_dim_exists (k : Type u_3) (𝔤 : Type u_4) [Field k] [LieRing 𝔤] [LieAlgebra k 𝔤] [Module.Finite k 𝔤] [Module.Free k 𝔤] [LieAlgebra.IsSemisimple k 𝔤] : ∃ (n : ℕ), Even n ∧ n < Module.finrank k 𝔤 - LieAlgebra.rank k 𝔤

theorem exists_regular_nilpotent (k : Type u_3) (𝔤 : Type u_4) [Field k] [LieRing 𝔤] [LieAlgebra k 𝔤] [Module.Finite k 𝔤] [Module.Free k 𝔤] [LieAlgebra.IsSemisimple k 𝔤] (h : LieAlgebra.rank k 𝔤 < Module.finrank k 𝔤) : ∃ x ∈ nilpotentCone k 𝔤, Module.finrank k ↥(LinearMap.ker ((LieAlgebra.ad k 𝔤) x)) = LieAlgebra.rank k 𝔤

theorem nilpotentCone_ne_singularLocus (k : Type u_3) (𝔤 : Type u_4) [Field k] [LieRing 𝔤] [LieAlgebra k 𝔤] [Module.Finite k 𝔤] [Module.Free k 𝔤] [LieAlgebra.IsSemisimple k 𝔤] : nilpotentCone k 𝔤 ≠ nilpotentCone_singularLocus k 𝔤

noncomputable def nilpotentCone_singLocus_dim (k : Type u_3) (𝔤 : Type u_4) [Field k] [LieRing 𝔤] [LieAlgebra k 𝔤] [Module.Finite k 𝔤] [Module.Free k 𝔤] [LieAlgebra.IsSemisimple k 𝔤] : ℕ

noncomputable def nilpotentCone_dimVariety (k : Type u_3) (𝔤 : Type u_4) [Field k] [LieRing 𝔤] [LieAlgebra k 𝔤] [Module.Finite k 𝔤] [Module.Free k 𝔤] [LieAlgebra.IsSemisimple k 𝔤] : Set 𝔤 → ℕ

theorem even_sub_even_of_lt_ge_two {m n : ℕ} (hm : Even m) (hn : Even n) (hlt : n < m) : m - n ≥ 2

theorem nilpotentCone_singular_codim_ge_two (k : Type u_3) (𝔤 : Type u_4) [Field k] [LieRing 𝔤] [LieAlgebra k 𝔤] [Module.Finite k 𝔤] [Module.Free k 𝔤] [LieAlgebra.IsSemisimple k 𝔤] (dimVariety : Set 𝔤 → ℕ) (hdim_nilpCone : dimVariety (nilpotentCone k 𝔤) = Module.finrank k 𝔤 - LieAlgebra.rank k 𝔤) (hdim_singLocus : dimVariety (nilpotentCone_singularLocus k 𝔤) = ⋯.choose) : dimVariety (nilpotentCone k 𝔤) - dimVariety (nilpotentCone_singularLocus k 𝔤) ≥ 2

structure NilpotentConeCoordRingData (k : Type u_3) (𝔤 : Type u_4) [Field k] [LieRing 𝔤] [LieAlgebra k 𝔤] : Type (max (max u_3 u_4) (u_5 + 1))

• SymAlg : Type u_5
• symAlgCommRing : CommRing self.SymAlg
• symAlgAlgebra : Algebra k self.SymAlg
• eval_𝔤 : self.SymAlg →ₐ[k] 𝔤 → k
• vanishingIdeal : Ideal self.SymAlg
• mem_vanishingIdeal (f : self.SymAlg) : f ∈ self.vanishingIdeal ↔ ∀ x ∈ nilpotentCone k 𝔤, self.eval_𝔤 f x = 0
• symAlg_isNoetherian : IsNoetherianRing self.SymAlg
• vanishingIdeal_isPrime : self.vanishingIdeal.IsPrime

@[reducible, inline]

abbrev NilpotentConeCoordRingData.coordRing {k : Type u_3} {𝔤 : Type u_4} [Field k] [LieRing 𝔤] [LieAlgebra k 𝔤] (D : NilpotentConeCoordRingData k 𝔤) : Type u_5

theorem nilpotentCone_coordRing_isDomain {k : Type u_3} {𝔤 : Type u_4} [Field k] [LieRing 𝔤] [LieAlgebra k 𝔤] [LieAlgebra.IsSemisimple k 𝔤] [Module.Finite k 𝔤] (D : NilpotentConeCoordRingData k 𝔤) : IsDomain D.coordRing

instance NilpotentConeCoordRingData.instIsDomainCoordRing {k : Type u_3} {𝔤 : Type u_4} [Field k] [LieRing 𝔤] [LieAlgebra k 𝔤] [LieAlgebra.IsSemisimple k 𝔤] [Module.Finite k 𝔤] (D : NilpotentConeCoordRingData k 𝔤) : IsDomain D.coordRing

instance NilpotentConeCoordRingData.instIsNoetherianCoordRing {k : Type u_3} {𝔤 : Type u_4} [Field k] [LieRing 𝔤] [LieAlgebra k 𝔤] (D : NilpotentConeCoordRingData k 𝔤) : IsNoetherianRing D.coordRing

def SatisfiesSerreR1 (R : Type u_3) [CommRing R] : Prop

def SatisfiesSerreS2 (R : Type u_3) [CommRing R] : Prop

theorem serre_criterion_normal {R : Type u_3} [CommRing R] [IsDomain R] [IsNoetherianRing R] (hR1 : SatisfiesSerreR1 R) (hS2 : SatisfiesSerreS2 R) : IsIntegrallyClosed R

theorem nilpotentCone_satisfies_R1 {k : Type u_3} {𝔤 : Type u_4} [Field k] [LieRing 𝔤] [LieAlgebra k 𝔤] [LieAlgebra.IsSemisimple k 𝔤] [Module.Finite k 𝔤] (D : NilpotentConeCoordRingData k 𝔤) : SatisfiesSerreR1 D.coordRing

theorem nilpotentCone_satisfies_S2 {k : Type u_3} {𝔤 : Type u_4} [Field k] [LieRing 𝔤] [LieAlgebra k 𝔤] [LieAlgebra.IsSemisimple k 𝔤] [Module.Finite k 𝔤] (D : NilpotentConeCoordRingData k 𝔤) : SatisfiesSerreS2 D.coordRing

theorem nilpotentCone_isNormal {k : Type u_3} {𝔤 : Type u_4} [Field k] [LieRing 𝔤] [LieAlgebra k 𝔤] [LieAlgebra.IsSemisimple k 𝔤] [Module.Finite k 𝔤] (D : NilpotentConeCoordRingData k 𝔤) : IsIntegrallyClosed D.coordRing

theorem normalVariety_singular_locus_codim_ge_two (R : Type u_3) [CommRing R] [IsDomain R] [IsNoetherianRing R] [IsIntegrallyClosed R] (𝔭 : Ideal R) [𝔭.IsPrime] (h𝔭 : 𝔭.height = 1) : IsRegularLocalRing (Localization.AtPrime 𝔭)

theorem normalVariety_extend_regular_function (R : Type u_3) [CommRing R] [IsDomain R] [IsNoetherianRing R] [IsIntegrallyClosed R] (x : FractionRing R) (hx : ∀ (𝔭 : Ideal R) [inst : 𝔭.IsPrime], 𝔭.height = 1 → x ∈ (algebraMap (Localization.AtPrime 𝔭) (FractionRing R)).range) : x ∈ (algebraMap R (FractionRing R)).range

opaque IsProperMorphism {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] (_f : R →+* S) : Prop

theorem normalVariety_zariski_main_theorem_connected_fibers (R : Type u_3) [CommRing R] [IsDomain R] [IsNoetherianRing R] [IsIntegrallyClosed R] (S : Type u_4) [CommRing S] [IsDomain S] (f : R →+* S) (hf_inj : Function.Injective ⇑f) (hf_proper : IsProperMorphism f) (hbir : ∃ (φ : FractionRing R ≃+* FractionRing S), ∀ (r : R), φ ((algebraMap R (FractionRing R)) r) = (algebraMap S (FractionRing S)) (f r)) (𝔭 : Ideal R) [𝔭.IsPrime] : ConnectedSpace (PrimeSpectrum (S ⧸ Ideal.map f 𝔭))

def IsGradedAlgEquiv {k : Type u_3} [CommSemiring k] {A : Type u_4} [Semiring A] [Algebra k A] {B : Type u_5} [Semiring B] [Algebra k B] (𝒜 : ℕ → Submodule k A) (ℬ : ℕ → Submodule k B) (e : A ≃ₐ[k] B) : Prop

structure ResolutionData (k : Type u_3) [Field k] : Type (max (max u_3 (u_4 + 1)) (u_5 + 1))

• OY : Type u_4
• oyCommRing : CommRing self.OY
• oyIsDomain : IsDomain self.OY
• oyAlgebra : Algebra k self.OY
• oyIntegrallyClosed : IsIntegrallyClosed self.OY
• oyNoetherian : IsNoetherianRing self.OY
• OX : Type u_5
• oxCommRing : CommRing self.OX
• oxIsDomain : IsDomain self.OX
• oxAlgebra : Algebra k self.OX
• pStar : self.OY →+* self.OX
• hProper : Algebra.IsIntegral self.OY self.OX
• hFracIso : ∃ (φ : FractionRing self.OY ≃+* FractionRing self.OX), ∀ (r : self.OY), φ ((algebraMap self.OY (FractionRing self.OY)) r) = (algebraMap self.OX (FractionRing self.OX)) (self.pStar r)

noncomputable def ResolutionData.mk' (k : Type u_3) [Field k] (OY : Type u_4) [CommRing OY] [IsDomain OY] [Algebra k OY] [IsIntegrallyClosed OY] [IsNoetherianRing OY] (OX : Type u_5) [CommRing OX] [IsDomain OX] [Algebra k OX] (pStar : OY →+* OX) (hProper : Algebra.IsIntegral OY OX) (hFracIso : ∃ (φ : FractionRing OY ≃+* FractionRing OX), ∀ (r : OY), φ ((algebraMap OY (FractionRing OY)) r) = (algebraMap OX (FractionRing OX)) (pStar r)) : ResolutionData k

theorem ResolutionData.pStar_injective {k : Type u_3} [Field k] (R : ResolutionData k) : Function.Injective ⇑R.pStar

theorem resolution_pullback_surjective {k : Type u_3} [Field k] (R : ResolutionData k) : Function.Surjective ⇑R.pStar

theorem resolution_pullback_isIso {k : Type u_3} [Field k] (R : ResolutionData k) : Function.Bijective ⇑R.pStar

theorem graded_map_reflects_mem {k : Type u_3} [Field k] {R : Type u_4} [CommRing R] [Algebra k R] {S : Type u_5} [CommRing S] [Algebra k S] (𝒜 : ℕ → Submodule k R) [GradedAlgebra 𝒜] (ℬ : ℕ → Submodule k S) [GradedAlgebra ℬ] (f : R →ₐ[k] S) (hf_grade : ∀ (n : ℕ), ∀ a ∈ 𝒜 n, f a ∈ ℬ n) (hf_inj : Function.Injective ⇑f) (n : ℕ) (a : R) (ha : f a ∈ ℬ n) : a ∈ 𝒜 n

theorem springer_pullback_isIso (D : SpringerResolutionData) (ON : Type u_3) [CommRing ON] [IsDomain ON] [Algebra D.k ON] [IsIntegrallyClosed ON] [IsNoetherianRing ON] (𝒩_grade : ℕ → Submodule D.k ON) [GradedAlgebra 𝒩_grade] (OTF : Type u_4) [CommRing OTF] [IsDomain OTF] [Algebra D.k OTF] (TF_grade : ℕ → Submodule D.k OTF) [GradedAlgebra TF_grade] (pstar : ON →ₐ[D.k] OTF) (hbirational : ∃ (φ : FractionRing ON ≃+* FractionRing OTF), ∀ (r : ON), φ ((algebraMap ON (FractionRing ON)) r) = (algebraMap OTF (FractionRing OTF)) (pstar r)) (hproper : Algebra.IsIntegral ON OTF) (hpstar_preserves_grade : ∀ (n : ℕ), ∀ f ∈ 𝒩_grade n, pstar f ∈ TF_grade n) : ∃ (e : ON ≃ₐ[D.k] OTF), (∀ (f : ON), e f = pstar f) ∧ IsGradedAlgEquiv 𝒩_grade TF_grade e