AlgebrasOverFields_GeometricallyIrreducibleAlgebra_transitive.lean`

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

Mathlib

class GeometricallyIrreducibleAlgebra line 41 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra
4 instances, coercions and auxiliary constants left out.
Also declared: APNOutputs/StacksProject/AlgebrasOverFields_GeometricallyIrreducibleAlgebra_of_directed_colimit.lean:41 (same declaration text), APNOutputs/StacksProject/AlgebrasOverFields_geometrically_irreducible_tfae.lean:41 (same declaration text), APNOutputs/StacksProject/AlgebrasOverFields_minimalPrimes_bijection_of_geometrically_IrreducibleAlgebra.lean:41 (same declaration text), APNOutputs/StacksProject/AlgebrasOverFields_unique_minimal_prime_of_tensor_product_of_separably_closed.lean:41 (same declaration text).
def alg_dir_lim line 46 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Preorder, IsDirected, LE.le, Nonempty, CommRing, Algebra, AlgHom, Ring.DirectLimit
Proof uses: Classical.arbitrary, RingHom, Ring.DirectLimit.of, RingHom.toAlgebra, RingHom.comp, algebraMap
17 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: APNOutputs/StacksProject/AlgebrasOverFields_GeometricallyIrreducibleAlgebra_of_directed_colimit.lean:46 (same statement text; different proof or body), APNOutputs/StacksProject/AlgebrasOverFields_geometrically_irreducible_tfae.lean:46 (same statement text; different proof or body), APNOutputs/StacksProject/AlgebrasOverFields_minimalPrimes_bijection_of_geometrically_IrreducibleAlgebra.lean:46 (same statement text; different proof or body), APNOutputs/StacksProject/AlgebrasOverFields_unique_minimal_prime_of_tensor_product_of_separably_closed.lean:46 (same statement text; different proof or body). Qualify references as alg_dir_lim@path.
lemma isNilpotent_of_mem_ideal_gen_by_nilpotents line 62 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Set, Membership.mem, IsNilpotent, Ideal, Ideal.span
Proof uses: Submodule, Submodule.span, Submodule.span_induction, IsNilpotent.zero, of_eq_true, HAdd.hAdd, Eq.trans, True, forall_congr, implies_congr_ctx, Eq.refl, eq_true, Commute.isNilpotent_add, Commute.all, implies_true, HMul.hMul, Commute.isNilpotent_mul_left
43 instances, coercions and auxiliary constants left out.
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma isPrime_nilradical_of_irreducibleSpace line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IrreducibleSpace, PrimeSpectrum, Ideal.IsPrime, nilradical
Proof uses: Eq.mpr, InfSet.sInf, Ideal, setOf, id, Eq, congrArg, nilradical_eq_sInf, And, Ne, Top.top, Membership.mem, HMul.hMul, Or, Eq.trans, funext, Set, forall_congr, implies_congr, congr and 42 more
36 instances, coercions and auxiliary constants left out.
Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma nil_of_base_change_surjective line 83 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, AlgHom, Function.Surjective, Eq, OfNat.ofNat, IsNilpotent, TensorProduct, Algebra.TensorProduct.map, AlgHom.id
Proof uses: Ideal, RingHom.ker, RingHom, LinearMap, RingHom.id, AlgHom.toLinearMap, LinearMap.comp, LinearMap.id, Exists, LinearMap.exists_rightInverse_of_surjective, Iff.mpr, Submodule, LinearMap.range, Top.top, LinearMap.range_eq_top, HSub.hSub, id, Eq.mpr, congrArg, map_sub and 40 more
148 instances, coercions and auxiliary constants left out.
Tactic trace: 56 steps
Open to load the checked before-and-after goal states.
lemma injective_of_base_change line 147 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, AlgHom, Function.Injective, TensorProduct, Algebra.TensorProduct.map, AlgHom.id
Proof uses: Module.Flat.lTensor_preserves_injective_linearMap, AlgHom.toLinearMap
64 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma irreducibleSpace_of_denseRange line 153 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, IrreducibleSpace, Continuous, DenseRange
Proof uses: Eq.mpr, IsIrreducible, Top.top, Set, id, Eq, congrArg, propext, irreducibleSpace_def, Set.univ, Iff.mp, Set.image, IsIrreducible.image, Continuous.continuousOn, Set.range, Set.image_univ, closure, IsIrreducible.closure, Eq.mp, DenseRange.closure_range
2 instances, coercions and auxiliary constants left out.
Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma irreducibleSpace_of_nilradical_isPrime line 166 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ideal.IsPrime, nilradical, IrreducibleSpace, PrimeSpectrum
Proof uses: Eq.mpr, IsIrreducible, Top.top, Set, id, Eq, And, Set.Nonempty, IsPreirreducible, IsClosed, HasSubset.Subset, Union.union, Or, congrArg, Exists, PrimeSpectrum.zeroLocus, forall_congr, implies_congr, Eq.refl, propext and 26 more
34 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma nilradical_comap_injective line 173 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingHom, Function.Injective, Eq, Ideal, Ideal.comap, nilradical
Proof uses: Ideal.ext, Eq.mpr, Iff, Membership.mem, IsNilpotent, id, congr, congrArg, Eq.trans, Iff.intro, Nat, HPow.hPow, OfNat.ofNat, Exists.intro, map_pow, map_zero, Eq.symm, Eq.refl
35 instances, coercions and auxiliary constants left out.
Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma irreducibleSpace_of_injective line 187 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingHom, Function.Injective, IrreducibleSpace, PrimeSpectrum
Proof uses: Ideal.IsPrime, nilradical, isPrime_nilradical_of_irreducibleSpace, Eq, Ideal, Ideal.comap, nilradical_comap_injective, Eq.mpr, id, congrArg, Eq.symm, Ideal.comap_isPrime, irreducibleSpace_of_nilradical_isPrime
13 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma nilradical_comap_surjective_nil line 196 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingHom, Eq, OfNat.ofNat, IsNilpotent, Ideal, Ideal.comap, nilradical
Proof uses: Ideal.ext, Eq.mpr, Iff, Membership.mem, id, congr, congrArg, Eq.trans, Iff.intro, Nat, HPow.hPow, map_pow, Eq.refl, Exists.intro, HMul.hMul, pow_mul, Eq.symm, map_zero
47 instances, coercions and auxiliary constants left out.
Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma irreducibleSpace_of_surjective_nil line 213 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingHom, Function.Surjective, Eq, OfNat.ofNat, IsNilpotent, IrreducibleSpace, PrimeSpectrum
Proof uses: Ideal.IsPrime, nilradical, isPrime_nilradical_of_irreducibleSpace, Ideal, Ideal.comap, nilradical_comap_surjective_nil, Eq.mpr, id, congrArg, Eq.symm, Ideal.comap_isPrime, irreducibleSpace_of_nilradical_isPrime
33 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma irreducibleSpace_of_equiv line 223 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingEquiv, IrreducibleSpace, PrimeSpectrum
Proof uses: Eq.mpr, IsIrreducible, Top.top, Set, id, Eq, congrArg, propext, irreducibleSpace_def, And, Set.Nonempty, IsOpen, Inter.inter, Exists, Compl.compl, PrimeSpectrum.zeroLocus, forall_congr, implies_congr, Eq.refl, And.intro and 62 more
66 instances, coercions and auxiliary constants left out.
Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
lemma exists_mvpolynomial_preimage_two line 244 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, TensorProduct, Exists, Nat, AlgHom, MvPolynomial, Fin, And, Eq, Algebra.TensorProduct.map, AlgHom.id
Proof uses: Eq.mpr, id, congrArg, funext, Eq.trans, Classical.byContradiction, Not, Finset, Prod, Finset.sum, TensorProduct.tmul, Prod.fst, Prod.snd, TensorProduct.exists_finset, False, Exists.intro, Equiv, Subtype, Membership.mem, Finset.card and 36 more
102 instances, coercions and auxiliary constants left out.
Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma lift_irred line 262 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, GeometricallyIrreducibleAlgebra, IrreducibleSpace, PrimeSpectrum, TensorProduct
Proof uses: Nontrivial, inferInstance, Ideal.IsPrime, nilradical, Ideal.IsPrime.mk, Eq, Ideal, Top.top, Membership.mem, OfNat.ofNat, Eq.mpr, id, congrArg, True.intro, Nat, HPow.hPow, False, one_pow, zero_ne_one, Eq.mp and 73 more
162 instances, coercions and auxiliary constants left out.
Tactic trace: 101 steps
Open to load the checked before-and-after goal states.
lemma irreducibleSpace_of_algEquiv line 369 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, AlgEquiv, IrreducibleSpace, PrimeSpectrum
Proof uses: irreducibleSpace_of_equiv
17 instances, coercions and auxiliary constants left out.
theorem GeometricallyIrreducibleAlgebra.transitive line 376 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, CommRing, IsScalarTower, GeometricallyIrreducibleAlgebra
Proof uses: GeometricallyIrreducibleAlgebra.mk, IrreducibleSpace, PrimeSpectrum, TensorProduct, lift_irred, Ideal.IsPrime, nilradical, isPrime_nilradical_of_irreducibleSpace, Exists, IsDomain, AlgHom, And, Function.Surjective, Eq, OfNat.ofNat, IsNilpotent, Exists.intro, HasQuotient.Quotient, Ideal, inferInstance and 28 more
88 instances, coercions and auxiliary constants left out.
Tactic trace: 38 steps
Open to load the checked before-and-after goal states.