AlgebrasOverFields_GeometricallyIrreducibleAlgebra_of_directed_colimit.lean`

GitHub source file

23 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_transitive.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_transitive.lean:46 (same statement text; different proof or body), APNOutputs/StacksProject/AlgebrasOverFields_geometrically_irreducible_tfae.lean:46 (same declaration text), APNOutputs/StacksProject/AlgebrasOverFields_minimalPrimes_bijection_of_geometrically_IrreducibleAlgebra.lean:46 (same declaration text), APNOutputs/StacksProject/AlgebrasOverFields_unique_minimal_prime_of_tensor_product_of_separably_closed.lean:46 (same declaration text). Qualify references as alg_dir_lim@path.
lemma preirred_univ_of_nilradical_prime line 60 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ideal.IsPrime, nilradical, IsPreirreducible, PrimeSpectrum, Set.univ
Proof uses: Set, IsOpen, Set.Nonempty, Inter.inter, Eq, Compl.compl, PrimeSpectrum.zeroLocus, Exists, Eq.mp, congrArg, propext, PrimeSpectrum.isOpen_iff, Eq.mpr, id, Eq.symm, compl_compl, Eq.refl, Ideal, Ideal.span, Ne and 44 more
55 instances, coercions and auxiliary constants left out.
Tactic trace: 132 steps
Open to load the checked before-and-after goal states.
lemma irred_of_nilradical_prime line 173 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ideal.IsPrime, nilradical, IrreducibleSpace, PrimeSpectrum
Proof uses: Ne, OfNat.ofNat, Eq, Membership.mem, Ideal, Eq.mpr, id, congrArg, Eq.symm, Ideal.zero_mem, Top.top, Ideal.eq_top_of_isUnit_mem, isUnit_one, Ideal.IsPrime.ne_top, IrreducibleSpace.mk, PreirreducibleSpace.mk, preirred_univ_of_nilradical_prime, inferInstance, Nonempty, nontrivial_of_ne
28 instances, coercions and auxiliary constants left out.
Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma nilradical_prime_iff line 186 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Iff, Ideal.IsPrime, nilradical, And, Not, IsNilpotent, OfNat.ofNat, HMul.hMul, Or
Proof uses: Iff.intro, And.intro, Membership.mem, Ideal, Eq, Top.top, Ideal.eq_top_of_isUnit_mem, isUnit_one, Ne, Ideal.IsPrime.ne_top, Ideal.IsPrime.mem_or_mem, Ideal.IsPrime.mk, Eq.mpr, id, congrArg, True.intro, And.left, And.right
45 instances, coercions and auxiliary constants left out.
Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma nilradical_prime_of_equiv line 207 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingEquiv, Ideal.IsPrime, nilradical
Proof uses: Iff.mpr, And, Not, IsNilpotent, OfNat.ofNat, HMul.hMul, Or, nilradical_prime_iff, Iff.mp, And.intro, Nat, Eq, HPow.hPow, Exists, Exists.intro, Eq.mpr, id, congrArg, Eq.symm, map_pow and 12 more
48 instances, coercions and auxiliary constants left out.
Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
lemma nilradical_prime_of_irreducibleSpace line 239 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IrreducibleSpace, PrimeSpectrum, Ideal.IsPrime, nilradical
Proof uses: Iff.mpr, And, Not, IsNilpotent, OfNat.ofNat, HMul.hMul, Or, nilradical_prime_iff, And.intro, Eq, Set, Set.univ, EmptyCollection.emptyCollection, Set.ext, Iff.intro, Membership.mem, Nat, HPow.hPow, Exists, Exists.intro and 60 more
57 instances, coercions and auxiliary constants left out.
Tactic trace: 131 steps
Open to load the checked before-and-after goal states.
lemma isPrime_nilradical_of_colimit_like line 350 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Preorder, IsDirected, LE.le, Nonempty, CommRing, RingHom, DirectedSystem, Ideal.IsPrime, nilradical, Eq, Exists, OfNat.ofNat
Proof uses: Ne, Ideal, Top.top, Membership.mem, Eq.mpr, id, congrArg, Submodule.mem_top, IsNilpotent, Nat, HPow.hPow, False, Exists.intro, Trans.trans, one_pow, Eq.refl, map_one, Ideal.eq_top_of_isUnit_mem, Eq.mp, Ideal.zero_mem and 14 more
60 instances, coercions and auxiliary constants left out.
Tactic trace: 79 steps
Open to load the checked before-and-after goal states.
def tensor_finsupp_equiv line 427 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, AddCommGroup, Module, DecidableEq, LinearEquiv, RingHom.id, TensorProduct, Finsupp
Proof uses: LinearEquiv.trans, TensorProduct.finsuppRight, Finsupp.mapRange.linearEquiv, TensorProduct.rid
73 instances, coercions and auxiliary constants left out.
def tensor_basis_equiv line 431 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, AddCommGroup, Module, Algebra, LinearEquiv, RingHom.id, TensorProduct, Finsupp, Module.Basis.ofVectorSpaceIndex
Proof uses: Module.Basis, Module.Basis.ofVectorSpace, Set, LinearEquiv.trans, TensorProduct.congr, LinearEquiv.refl, Module.Basis.repr, tensor_finsupp_equiv, Classical.decEq
64 instances, coercions and auxiliary constants left out.
lemma map_tensor_basis_equiv line 438 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, AddCommGroup, Module, Algebra, LinearMap, RingHom.id, TensorProduct, Eq, Finsupp, Module.Basis.ofVectorSpaceIndex, LinearEquiv, tensor_basis_equiv, TensorProduct.map, LinearMap.id, Finsupp.mapRange.linearMap
Proof uses: Finsupp.ext, TensorProduct.induction_on, Membership.mem, Set, OfNat.ofNat, of_eq_true, Subtype.mk, Eq.trans, True, congr, congrArg, map_zero, RingHom, Finsupp.mapRange_zero, LinearMap.map_zero, eq_self, eq_true, True.intro, id, TensorProduct.tmul and 10 more
124 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma tensor_mem_range_of_finset line 446 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, TensorProduct, Exists, Finset, AlgHom, Membership.mem, Submodule, LinearMap.range, RingHom.id, AlgHom.toLinearMap, Subalgebra, AlgHom.range, Algebra.TensorProduct.map, AlgHom.id
Proof uses: TensorProduct.induction_on, Exists.intro, OfNat.ofNat, EmptyCollection.emptyCollection, Eq, RingHom, AlgHom.toRingHom, map_zero, TensorProduct.tmul, Singleton.singleton, Finset.mem_singleton_self, LinearMap, id, Eq.mpr, congrArg, Eq.refl, HAdd.hAdd, Union.union, Classical.decEq, Finset.mem_union_left and 2 more
100 instances, coercions and auxiliary constants left out.
Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma finset_subfield_equiv line 478 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Finset, Exists, AlgHom, Membership.mem, Submodule, LinearMap.range, RingHom.id, AlgHom.toLinearMap
Proof uses: Equiv, Subtype, Fin, Fintype.card, Fintype.equivFin, MvPolynomial, MvPolynomial.aeval, Equiv.symm, Ideal, RingHom.ker, RingHom, AlgHom.toRingHom, Ideal.IsPrime, RingHom.ker_isPrime, HasQuotient.Quotient, FractionRing, RingHom.kerLift, Function.Injective, RingHom.kerLift_injective, nonZeroDivisors and 19 more
64 instances, coercions and auxiliary constants left out.
Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
def uliftRingEquiv line 517 source
no axioms what this means
Statement uses: CommRing, RingEquiv, ULift
Proof uses: Equiv, Equiv.symm, Equiv.ulift, RingEquiv.mk
20 instances, coercions and auxiliary constants left out.
def SmallFieldLift line 522 source
no axioms what this means
Proof uses: ULift
instance (instance at line 524) line 524 source
instance (instance at line 527) line 527 source
instance (instance at line 530) line 530 source
lemma geom_irred_universe_lift_one line 533 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, GeometricallyIrreducibleAlgebra, Not, IsNilpotent, TensorProduct, OfNat.ofNat
Proof uses: Nat, Eq, HPow.hPow, False, Trans.trans, Eq.mpr, id, congrArg, one_pow, Eq.refl, IrreducibleSpace, PrimeSpectrum, SmallFieldLift, GeometricallyIrreducibleAlgebra.out, Ne, Nonempty, inferInstance, Ideal.IsPrime, PrimeSpectrum.asIdeal, Ideal and 14 more
99 instances, coercions and auxiliary constants left out.
Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
lemma nilradical_prime_of_directed_colimit_tensor line 579 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Preorder, IsDirected, LE.le, Nonempty, CommRing, Algebra, AlgHom, DirectedSystem, Ring.DirectLimit, Ideal.IsPrime, TensorProduct, nilradical, Eq, RingHom, algebraMap, RingHom.comp, Classical.arbitrary, Ring.DirectLimit.of
Proof uses: Algebra.TensorProduct.map, AlgHom.id, AlgHom.toRingHom, inferInstanceAs, DirectedSystem.mk, LinearMap, RingHom.id, AlgHom.toLinearMap, le_refl, TensorProduct.ext', DirectedSystem.map_self', id, TensorProduct.tmul, Eq.mpr, congrArg, Eq.refl, AlgHom.ext, LinearMap.congr_fun, AlgHom.congr_fun, LinearMap.comp and 64 more
129 instances, coercions and auxiliary constants left out.
Tactic trace: 161 steps
Open to load the checked before-and-after goal states.
lemma geom_irred_universe_lift_prime line 741 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, GeometricallyIrreducibleAlgebra, TensorProduct, IsNilpotent, HMul.hMul, Or
Proof uses: Exists, Finset, AlgHom, Membership.mem, Submodule, LinearMap.range, RingHom.id, AlgHom.toLinearMap, Subalgebra, AlgHom.range, Algebra.TensorProduct.map, AlgHom.id, tensor_mem_range_of_finset, Union.union, Classical.decEq, finset_subfield_equiv, Finset.mem_union_left, Finset.mem_union_right, Eq, RingHom and 58 more
124 instances, coercions and auxiliary constants left out.
Tactic trace: 68 steps
Open to load the checked before-and-after goal states.
lemma geom_irred_universe_lift line 813 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, GeometricallyIrreducibleAlgebra, Ideal.IsPrime, TensorProduct, nilradical
Proof uses: Iff.mpr, And, Not, IsNilpotent, OfNat.ofNat, HMul.hMul, Or, nilradical_prime_iff, And.intro, geom_irred_universe_lift_one, geom_irred_universe_lift_prime
52 instances, coercions and auxiliary constants left out.
Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem GeometricallyIrreducibleAlgebra.of_directed_colimit line 825 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Preorder, IsDirected, LE.le, Nonempty, CommRing, Algebra, AlgHom, DirectedSystem, GeometricallyIrreducibleAlgebra, Ring.DirectLimit, alg_dir_lim
Proof uses: GeometricallyIrreducibleAlgebra.mk, Ideal.IsPrime, TensorProduct, nilradical, geom_irred_universe_lift, nilradical_prime_of_directed_colimit_tensor, rfl, RingHom, algebraMap, irred_of_nilradical_prime
35 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.