GeometricIrreducibility.lean

lemma Ideal.under_mem_minimalPrimes (R : Type*) {S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.HasGoingDown R S] (p : Ideal S) (hp : p ∈ minimalPrimes S) :
    p.under R ∈ minimalPrimes R

lemma Algebra.TensorProduct.exists_intermediateField_isSeparable_and_mem_range
    (Ω : Type*) [Field Ω] [Algebra k Ω] [Algebra.IsSeparable k Ω] (x : Ω ⊗[k] R) :
    ∃ (K : IntermediateField k Ω), Algebra.IsSeparable k K ∧ Module.Finite k K ∧
        x ∈ Set.range
          (Algebra.TensorProduct.map (IsScalarTower.toAlgHom k K Ω) (AlgHom.id k R))

lemma Algebra.TensorProduct.exists_field_isSeparable_and_mem_range (Ω : Type v) [Field Ω]
    [Algebra k Ω] [Algebra.IsSeparable k Ω] (x : Ω ⊗[k] R) :
    ∃ (K : Type v) (_ : Field K) (_ : Algebra k K) (_ : Algebra K Ω) (_ : IsScalarTower k K Ω),
      Algebra.IsSeparable k K ∧ Module.Finite k K ∧
        x ∈ Set.range
          (Algebra.TensorProduct.map (IsScalarTower.toAlgHom k K Ω) (AlgHom.id k R))

lemma subsingleton_minimalPrimes_of_isSeparable
    (H : ∀ (K : Type v) [Field K] [Algebra k K] [Module.Finite k K] [Algebra.IsSeparable k K],
      (minimalPrimes (K ⊗[k] R)).Subsingleton) (Ω : Type v) [Field Ω] [Algebra k Ω]
      [Algebra.IsSeparable k Ω] :
    (minimalPrimes (Ω ⊗[k] R)).Subsingleton

instance (priority := 100) PreirreducibleSpace.of_isEmpty (X : Type*) [TopologicalSpace X]
    [IsEmpty X] : PreirreducibleSpace X

lemma irreducibleSpace_iff_subsingleton_and_nonempty {X : Type*} [TopologicalSpace X] :
    IrreducibleSpace X ↔
      (irreducibleComponents X).Subsingleton ∧ (irreducibleComponents X).Nonempty

lemma preirreducibleSpace_iff_subsingleton_irreducibleComponents {X : Type*} [TopologicalSpace X] :
    PreirreducibleSpace X ↔ (irreducibleComponents X).Subsingleton

lemma PrimeSpectrum.preirreducibleSpace_iff {R : Type*} [CommSemiring R] :
    PreirreducibleSpace (PrimeSpectrum R) ↔ (minimalPrimes R).Subsingleton

lemma PrimeSpectrum.irreducibleSpace_iff {R : Type*} [CommSemiring R] :
    IrreducibleSpace (PrimeSpectrum R) ↔
      (minimalPrimes R).Subsingleton ∧ (minimalPrimes R).Nonempty

lemma Ideal.IsPrime.nontrivial {R : Type*} [Semiring R]
    {I : Ideal R} (hI : I.IsPrime) : Nontrivial R

lemma RingHom.isIntegral_algebraMap_iff {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] :
    (algebraMap R S).IsIntegral ↔ Algebra.IsIntegral R S

lemma Algebra.TensorProduct.isIntegral_includeRight (R S T : Type*) [CommRing R] [CommRing S]
    [Algebra R S] [CommRing T] [Algebra R T] [Algebra.IsIntegral R T] :
    (Algebra.TensorProduct.includeRight : S →ₐ[R] T ⊗[R] S).IsIntegral

lemma PrimeSpectrum.irreducibleSpace_of_isSeparable
    (H : ∀ (K : Type u) [Field K] [Algebra k K] [Module.Finite k K] [Algebra.IsSeparable k K],
      IrreducibleSpace (PrimeSpectrum (K ⊗[k] R))) (Ω : Type u) [Field Ω] [Algebra k Ω]
      [Algebra.IsSeparable k Ω] :
    IrreducibleSpace (PrimeSpectrum (Ω ⊗[k] R))

lemma PrimeSpectrum.comap_quotientMk_surjective_of_le_nilradical {R : Type*} [CommRing R]
    (I : Ideal R) (hle : I ≤ nilradical R) :
    Function.Surjective (PrimeSpectrum.comap <| Ideal.Quotient.mk I)

instance Subsingleton.charP (R : Type*) [AddMonoidWithOne R] [Subsingleton R] : CharP R 1

lemma nontrivial_of_expChar (R : Type*) [AddMonoidWithOne R] (q : ℕ) [hq : ExpChar R q] :
    Nontrivial R

lemma IsPurelyInseparable.of_surjective {F E : Type*} [CommRing F] [CommRing E] [Algebra F E]
    (h : Function.Surjective (algebraMap F E)) :
    IsPurelyInseparable F E where
  isIntegral := Algebra.isIntegral_of_surjective h
  inseparable' _ _ := h _

lemma PrimeSpectrum.irreducibleSpace_of_isAlgClosure_of_irreducibleSpace_of_isSepClosure
    (k R : Type*) [CommRing R] [Field k] [Algebra k R]
    (K : Type*) [Field K] [Algebra k K] [IsSepClosure k K]
    (L : Type*) [Field L] [Algebra k L] [IsAlgClosure k L] :
    IrreducibleSpace (PrimeSpectrum (K ⊗[k] R)) ↔ IrreducibleSpace (PrimeSpectrum (L ⊗[k] R))